:: deftheorem Def4 defines "\/" MSUALG_5:def 4 :
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, b₅ being Equivalence_Relation of M holds
( b₅ = EqR1 "\/" EqR2 iff ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 (\/) EqR2 & b₅ = EqCl EqR3 ) );