...

diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma
index ba2d65ba0cb32dfe84fd3d47f248eb1289652930..f47323e000f2fea00e57e3e29d7a8d15e643a34e 100644 (file)
--- a/helm/software/matita/library/formal_topology/formal_topologies.ma
+++ b/helm/software/matita/library/formal_topology/formal_topologies.ma
@@ -84,12 +84,14 @@ definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 
 
 coercion cr''.
 
-(*
-theorem C1':
+definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
+ λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
+
+coercion cr'''.
+
+axiom C1':
  ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
   extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
- intros;
-qed.
 
 definition formal_map_composition:
  ∀o1,o2,o3: formal_topology.
@@ -103,5 +105,17 @@ definition formal_map_composition:
      | intros;
        apply (.= (extS_com ??? c c1 ?));
        apply (.= †(C1 ?????));
-       apply (.= (C1 ?????));
-*)
\ No newline at end of file
+       apply (.= (C1' ?????));
+       apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
+       apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
+       apply (.= (extS_singleton ????)‡(extS_singleton ????));
+       apply refl1;
+     | apply (.= (extS_com ??? c c1 ?));
+       apply (.= (†(C2 ???)));
+       apply (.= (C2 ???));
+       apply refl1;]
+  | intros; simplify;
+    change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
+    apply prop1; assumption]
+qed.
+