+ {c | ext ? c ⊆ ext ? a ∩ ext ? b }.
+
+interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
+
+definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp ≝
+ λo,x,S. ∃y. y ∈ S ∧ x ⊩ y.
+
+interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).
+
+definition convergence ≝
+ λo: basic_pair.∀a: concr o.∀U,V: form o. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V).
\ No newline at end of file