The functor from BP to OBP has been defined (but no property proved yet).

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 071892f6bd3b7605f1892f450bd684915507e333..058176f4ce4556e07a5d10dc08049f05d59948c9 100644 (file)
--- 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