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 x' = x, y' = y as Equivalence_Relation of A by MSUALG_7:1;
A1: ( x' /\ y' = x' iff x' c= y' ) by XBOOLE_1:17, XBOOLE_1:28;
x "/\" y = the L_meet of (EqRelLatt A) . x',y' by LATTICES:def 2
.= x' /\ y' by MSUALG_5:def 2 ;
hence ( x [= y iff x c= y ) by A1, LATTICES:21; :: thesis: verum