1) as usual, I took the reverse notation for composition.

[helm.git] / helm / software / matita / library / formal_topology / relations.ma

diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index 72e12aa9dc500009518aebf7fb7038f629821771..1ab9ec3f15f9e810afc1c7c2093a625beaf05a48 100644 (file)
--- 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;