- [ apply (orelation_of_relation ?? (r \sub \c));
- | apply (orelation_of_relation ?? (r \sub \f));
- | lapply (commute ?? r);
- lapply (orelation_of_relation_preserves_equality ???? Hletin);
- apply (.= (orelation_of_relation_preserves_composition (concr BP1) ??? (rel BP2)) ^ -1);
- apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r)));
- apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ]
+ [ apply (t \sub \f);
+ | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+ apply sym1;
+ apply (.= †(†e));
+ change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
+ cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
+ cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+ apply (.= †COM);
+ change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
+ apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
+ apply (.= COM ^ -1);
+ change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
+ change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
+ apply (†e^-1);
+ | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+ apply sym1;
+ apply (.= †(†e));
+ change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
+ cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
+ cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+ apply (.= †COM);
+ change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
+ apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
+ apply (.= COM ^ -1);
+ change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
+ change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
+ apply (†e^-1);]
+qed.
+
+
+definition OR : carr3 (arrows3 CAT2 OBP OBTop).
+constructor 1;
+[ apply o_basic_topology_of_o_basic_pair;
+| intros; constructor 1;
+ [ apply o_continuous_relation_of_o_relation_pair;
+ | apply hide;
+ intros; whd; unfold o_continuous_relation_of_o_relation_pair; simplify;;
+ change with ((a \sub \f ⎻* ∘ oA (o_basic_topology_of_o_basic_pair S)) =
+ (a' \sub \f ⎻*∘ oA (o_basic_topology_of_o_basic_pair S)));
+ whd in e; cases e; clear e e2 e3 e4;
+ change in ⊢ (? ? ? (? ? ? ? ? % ?) ?) with ((⊩\sub S)⎻* ∘ (⊩\sub S)⎻);
+ apply (.= (comp_assoc2 ? ???? ?? a\sub\f⎻* ));
+ change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a\sub\f ∘ ⊩\sub S)⎻*;
+ apply (.= #‡†(Ocommute:?)^-1);
+ apply (.= #‡e1);
+ change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (⊩\sub T ∘ a'\sub\c)⎻*;
+ apply (.= #‡†(Ocommute:?));
+ change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a'\sub\f⎻* ∘ (⊩\sub S)⎻* );
+ apply (.= (comp_assoc2 ? ???? ?? a'\sub\f⎻* )^-1);
+ apply refl2;]
+| intros 2 (o a); apply refl1;
+| intros 6; apply refl1;]