Towards fullness.

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 f90b8bbbabec709d0c72e0d95f6872dc89d9e4fb..729f2894b845b1414952e55342d1b851f6f86b75 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
@@ -23,7 +23,35 @@ lemma rOR_full :
   ∀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 (h H1 H2); clear f; simplify;
+intro; cases s (s_2 s_1 s_eq); clear s; cases s_eq; clear s_eq s_2;
+intro; cases t (t_2 t_1 t_eq); clear t; cases t_eq; clear t_eq t_2;
+whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
+intro; whd in s_1 t_1;
+letin y ≝ (f⎻* ); clearbody y;
+ change in y with (carr2 (POW (form s_1) ⇒ POW (form t_1)));
+alias symbol "Vdash" = "basic pair relation for subsets (non applied)".
+letin z ≝ (image ?? (⊩ \sub s_1)); clearbody z;
+change in z with ((POW (concr s_1) → POW (form s_1)));
+ (*change in z with (carr2 (POW (concr s_1) ⇒ POW (form s_1)));*)
+
+ letin R ≝ (y ∘ z);
+
+ letin R ≝ (f* );∘ (⊩ \sub s_1));
+
+
+whd in ⊢ (? % ?→?); 
+whd in ⊢ (? % ?→?);  cases s_eq; intro; whd in f;
+simplify;
+intro; cases f (g H1 H2); clear f; exists;
+ [ constructor 1;
+    [
+    | unfold F1; simplify;
+    |
+    ]
+ |
+ ]
+
+ cases f (h H1 H2); clear f; simplify;
 change in ⊢ (? ? (λg:?.? ? ? (? ? ? %) ?)) with 
   (o_continuous_relation_of_o_relation_pair ?? (ℳ_2 g)).