X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fbin%2Fcomb.ml;h=f998b88a98934ee324b0c7516fe9f55d34ff5d5a;hb=601baed778a190b580982b588ebe49ba3f762b30;hp=5734c618d9b4126f92af9ec6cb62f6f8e3b737f5;hpb=cb99a2022db2d4731679912db78fba002c1acb5c;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/bin/comb.ml b/helm/software/matita/contribs/formal_topology/bin/comb.ml
index 5734c618d..f998b88a9 100755
--- 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