-definition overlaps ≝ λA:Type.λU,V:2 \sup A.∃a:A. a ∈ U ∧ a ∈ V.
-
-notation "hvbox(a break ≬ b)" non associative with precedence 45
-for @{ 'overlaps $a $b }.
-
-interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
-
-definition intersects ≝ λA:Type.λU,V:2 \sup A.mk_powerset ? (λa:A. a ∈ U ∧ a ∈ V).
-
-notation "hvbox(a break ∩ b)" non associative with precedence 55
-for @{ 'intersects $a $b }.
-
-interpretation "intersects" 'intersects U V = (intersects _ U V).
-
-definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U).