X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Frelations.ma;h=1ab9ec3f15f9e810afc1c7c2093a625beaf05a48;hb=1110bdf814f976ef0a36a024d2cba847ce06347e;hp=72e12aa9dc500009518aebf7fb7038f629821771;hpb=dd7f52dfd7f80b80368661fce5b58b644c102d7b;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index 72e12aa9d..1ab9ec3f1 100644
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -154,7 +154,7 @@ lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
         | change with (a = a); apply refl]]]
 qed.
 
-lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c1 ∘ c2) S = extS o1 o2 c1 (extS o2 o3 c2 S).
+lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (extS o2 o3 c2 S).
  intros; unfold extS; simplify; split; intros; simplify; intros;
   [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
     cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;