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

( 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