- [ 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;
+ lapply (.= †e); [3: apply rule t \sub \f; |4: apply Hletin; |1,2: skip]
+ cut ((t \sub \f ∘ (⊩)) ∘ (⊩)* = ?);
+ [
+
+ lapply (Hcut U); apply Hletin;
+ whd in Hcut;: apply rule (rel BP2);
+
+ generalize in match U; clear e;
+ change with (t \sub \f ((⊩) ((⊩)* U)) =(⊩) ((⊩)* (t \sub \f U)));
+ change in ⊢ (? ? ? % ?) with ((t \sub \f ∘ ((⊩) ∘ (⊩)* )) U);
+
+
+ | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
+ lapply (.= †e); [3: apply rule (t \sub \f ⎻* ); |4: apply Hletin; |1,2: skip]
+ change with (t \sub \f ⎻* ((⊩)⎻* ((⊩)⎻ U)) = (⊩)⎻* ((⊩)⎻ (t \sub \f⎻* U)));
+
+ ]
+qed.
\ No newline at end of file