-(*
-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;
+theorem BTop_to_OBTop_faithful: faithful2 ?? BTop_to_OBTop.
+ intros 5; apply (continuous_relation_eq_inv' o1 o2 f g); apply e;