-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).
-
-notation "↓a" with precedence 80 for @{ 'downarrow $a }.
-
-interpretation "downarrow" 'downarrow a = (downarrow _ a).
-
-definition fintersects ≝ λA:axiom_set.λU,V:2 \sup A.↓U ∩ ↓V.
-
-notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
-
-interpretation "fintersects" 'fintersects U V = (fintersects _ U V).