- [ 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) ?); ]
-qed.
+ [ apply (t \sub \f);
+ | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+ apply sym1;
+ alias symbol "refl" = "refl1".
+ apply (.= †?); [1: apply (t \sub \f (((◊_BP1∘(⊩)* ) U))); |
+ lapply (†e); [2: apply rule t \sub \f; | skip | apply Hletin]]
+ change in ⊢ (? ? ? % ?) with ((◊_BP2 ∘(⊩)* ) ((t \sub \f ∘ (◊_BP1∘(⊩)* )) U));
+ lapply (comp_assoc2 ????? (⊩)* (⊩) t \sub \f);
+ apply (.= †(Hletin ?)); clear Hletin;
+ change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
+ cut ?;
+ [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e3 ^ -1 ((⊩)* U));] | 2,4: skip]
+ apply (.= †Hcut);
+ change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
+ apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
+ apply (.= Hcut ^ -1);
+ change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
+ apply (prop11 ?? t \sub \f);
+ apply (e ^ -1);
+ | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+ apply sym1;
+ apply (.= †?); [1: apply (t \sub \f⎻* ((((⊩)⎻* ∘ (⊩)⎻) U))); |
+ lapply (†e); [2: apply rule (t \sub \f⎻* ); | skip | apply Hletin]]
+ change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘(⊩)⎻ ) ((t \sub \f⎻* ∘ ((⊩)⎻*∘(⊩)⎻ )) U));
+ lapply (comp_assoc2 ????? (⊩)⎻ (⊩)⎻* t \sub \f⎻* );
+ apply (.= †(Hletin ?)); clear Hletin;
+ change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
+ cut ?;
+ [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e1 ^ -1 ((⊩)⎻ U));] | 2,4: skip]
+ apply (.= †Hcut);
+ change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
+ apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
+ apply (.= Hcut ^ -1);
+ change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
+ apply (prop11 ?? t \sub \f⎻* );
+ apply (e ^ -1); ]
+qed.
\ No newline at end of file