theorem Th8: :: MSUALG_5:8

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