:: deftheorem Def2 defines EqRelLatt MSUALG_5:def 2 :
for X being set
for b₂ being strict Lattice holds
( b₂ = EqRelLatt X iff ( the carrier of b₂ = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b₂ . (x,y) = x /\ y & the L_join of b₂ . (x,y) = x "\/" y ) ) ) );