theorem :: MSUALG_5:7

for I being non empty set
for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR