(* *)
(**************************************************************************)
+include "basics/core_notation/fintersects_2.ma".
+include "basics/core_notation/downarrow_1.ma".
include "formal_topology/o-basic_topologies.ma".
-
+(*
(*
(*
definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
apply prop1; assumption]
qed.
*)
+*)