let X be set ; :: thesis: for x, y being Element of (BooleLatt X) holds
( x [= y iff x c= y )
let x, y be Element of (BooleLatt X); :: thesis: ( x [= y iff x c= y )
( x [= y iff x "\/" y = y ) by LATTICES:def 3;
hence ( x [= y iff x c= y ) by XBOOLE_1:7, XBOOLE_1:12; :: thesis: verum