for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds
EqR1 "\/" EqR2 c= EqR