(* *)
(**************************************************************************)
+include "basics/core_notation/fintersects_2.ma".
include "formal_topology/relations.ma".
include "formal_topology/notation.ma".
-
+(*
record basic_pair: Type[1] ≝ {
concr: REL; form: REL; rel: concr ⇒_\r1 form
}.
interpretation "basic pair relation for subsets" 'Vdash2 x y c = (fun21 (concr ?) ?? (relS c) x y).
interpretation "basic pair relation for subsets (non applied)" 'Vdash c = (fun21 ??? (relS c)).
*)
+*)