(**************************************************************************)
include "formal_topology/basic_topologies.ma".
-
+(*
(*
definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
intros; constructor 1;
apply prop1; assumption]
qed.
-*)
\ No newline at end of file
+*)
+*)