more polishing

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / r-o-basic_pairs.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index 1dcc1b91fe3c8a1c45746453190a1c16151c5faa..f90b8bbbabec709d0c72e0d95f6872dc89d9e4fb 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -20,10 +20,13 @@ definition rOBP ≝ Apply ?? BP_to_OBP.
 include "o-basic_pairs_to_o-basic_topologies.ma".
 
 lemma rOR_full : 
-  ∀rS,rT:rOBP.∀f:arrows2 BTop (OR (ℱ_2 rS)) (OR (ℱ_2 rT)).
-    exT22 ? (λg:arrows2 rOBP rS rT.
+  ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
+    exT22 ? (λg:arrows2 rOBP s t.
        map_arrows2 ?? OR ?? (ℳ_2 g) = f).
-intros; cases f (c H1 H2); simplify;
+intros; cases f (h H1 H2); clear f; simplify;
+change in ⊢ (? ? (λg:?.? ? ? (? ? ? %) ?)) with 
+  (o_continuous_relation_of_o_relation_pair ?? (ℳ_2 g)).
+
 STOP;