- [ apply (orelation_of_relation ?? c);
- | apply (reduced ?? c);
- | apply (saturated ?? c); ]
+ [ apply o_basic_topology_of_basic_topology;
+ | intros; apply o_continuous_relation_of_continuous_relation_morphism;
+ | cases daemon (*apply o_relation_topology_of_relation_topology_morphism_respects_id*);
+ | cases daemon (*apply o_relation_topology_of_relation_topology_morphism_respects_comp*);]
+qed.
+
+(*
+alias symbol "eq" (instance 2) = "setoid1 eq".
+alias symbol "eq" (instance 1) = "setoid2 eq".
+theorem BTop_to_OBTop_faithful:
+ ∀S,T.∀f,g:arrows2 (category2_of_category1 BTop) S T.
+ map_arrows2 ?? BTop_to_OBTop ?? f = map_arrows2 ?? BTop_to_OBTop ?? g → f=g.
+ intros; change with (∀b.A ? (ext ?? f b) = A ? (ext ?? g b));
+ apply (POW_faithful);
+ apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) f \sub \c (⊩ \sub T));
+ apply sym2;
+ apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) g \sub \c (⊩ \sub T));
+ apply sym2;
+ apply e;