More details on the proof.

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 5734c618d9b4126f92af9ec6cb62f6f8e3b737f5..f998b88a98934ee324b0c7516fe9f55d34ff5d5a 100755 (executable)
--- a/helm/software/matita/contribs/formal_topology/bin/comb.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/comb.ml
@@ -16,6 +16,16 @@ cMw = CMw
 -MMw = -w
 -MCw = MMCw
 iw = w
+
+
+  s <= s'            s <= s'         s <= s'           s <= s'
+===========        ===========     ============      ==========
+ ws <= Cws'         Cs <= Cs'       CMs' <= Ms       Ms' <= MCs
+
+  s <= s'          s <= s'
+===========     ============
+ s <= MMs'        Ms' <= Ms
+
 *)
 
 type t = M | I | C