X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_pairs.ma;h=058176f4ce4556e07a5d10dc08049f05d59948c9;hb=dba85ad7c7510e7bfd01e5721c63dad528b3e0bf;hp=071892f6bd3b7605f1892f450bd684915507e333;hpb=fdc6fe20875e45ea7446516af8904e2fb9b15388;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
index 071892f6b..058176f4c 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -203,6 +203,9 @@ definition o_relation_pair_of_relation_pair:
  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