let A be set ; :: thesis: for x, y being Element of (EqRelLatt A) holds
( x [= y iff x c= y )
let x, y be Element of (EqRelLatt A); :: thesis: ( x [= y iff x c= y )
reconsider x9 = x, y9 = y as Equivalence_Relation of A by MSUALG_5:21;
A1: ( x9 /\ y9 = x9 iff x9 c= y9 ) by XBOOLE_1:17, XBOOLE_1:28;
x "/\" y = the L_meet of (EqRelLatt A) . (x9,y9) by LATTICES:def 2
.= x9 /\ y9 by MSUALG_5:def 2 ;
hence ( x [= y iff x c= y ) by A1, LATTICES:4; :: thesis: verum