:: deftheorem Def5 defines EqRelLatt MSUALG_5:def 5 :
for I being non empty set
for M being ManySortedSet of I
for b₃ being strict Lattice holds
( b₃ = EqRelLatt M iff ( ( for x being set holds
( x in the carrier of b₃ iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b₃ . (x,y) = x (/\) y & the L_join of b₃ . (x,y) = x "\/" y ) ) ) );