+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).