+ }.
+
+definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
+
+coercion bt'.
+
+definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
+ intros; constructor 1;
+ [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
+ | intros; apply (.= (†H)‡(†H1)); apply refl1]
+qed.
+
+interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
+
+record formal_map (S,T: formal_topology) : Type ≝
+ { cr:> continuous_relation S T;
+ C1: ∀b,c. extS ?? cr (b ↓ c) = (ext ?? cr b) ↓ (ext ?? cr c);
+ C2: extS ?? cr T = S