-definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
-
-notation "hvbox(a break ∈ b)" non associative with precedence 45
-for @{ 'mem $a $b }.
-
-interpretation "mem" 'mem a S = (mem _ S a).
-
-definition overlaps ≝ λA:Type.λU,V:2 \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
-
-notation "hvbox(a break ≬ b)" non associative with precedence 45
-for @{ 'overlaps $a $b }. (* \between *)
-
-interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
-
-definition subseteq ≝ λA:Type.λU,V:2 \sup A.∀a:A. a ∈ U → a ∈ V.
-
-notation "hvbox(a break ⊆ b)" non associative with precedence 45
-for @{ 'subseteq $a $b }. (* \subseteq *)
-
-interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
-
-definition intersects ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∧ a ∈ V}.
-
-notation "hvbox(a break ∩ b)" non associative with precedence 55
-for @{ 'intersects $a $b }. (* \cap *)
-
-interpretation "intersects" 'intersects U V = (intersects _ U V).
-
-definition union ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∨ a ∈ V}.
-
-notation "hvbox(a break ∪ b)" non associative with precedence 55
-for @{ 'union $a $b }. (* \cup *)
-
-interpretation "union" 'union U V = (union _ U V).