+include "logic/equality.ma".
+include "logic/cprop_connectives.ma".
+
+record powerset (A : Type) : Type ≝ { char : A → CProp }.
+
+interpretation "char" 'subset p = (mk_powerset _ p).
+
+interpretation "pwset" 'powerset a = (powerset a).
+
+interpretation "in" 'mem a X = (char _ X a).
+
+definition subseteq ≝ λA.λu,v:\Omega \sup A.∀x.x ∈ u → x ∈ v.
+
+interpretation "subseteq" 'subseteq u v = (subseteq _ u v).
+
+definition overlaps ≝ λA.λU,V : Ω \sup A. exT2 ? (λx.x ∈ U) (λx.x ∈ V).
+
+interpretation "overlaps" 'overlaps u v = (overlaps _ u v).
+
+definition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
+
+interpretation "intersect" 'intersects u v = (intersect _ u v).