:: deftheorem Def3 defines EqRelSet MSUALG_8:def 3 :
for I being non empty set
for M being ManySortedSet of I
for i being Element of I
for X being Subset of (EqRelLatt M)
for b₅ being Subset of (EqRelLatt (M . i)) holds
( b₅ = EqRelSet (X,i) iff for x being set holds
( x in b₅ iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) );