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