constructor 1;
[ 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.
\ No newline at end of file