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 implies x "\/" y = y ) & ( x "\/" y = y implies x [= y ) & x "\/" y = x \/ y ) by LATTICES:def 3;
hence ( x [= y iff x c= y ) by XBOOLE_1:7, XBOOLE_1:12; :: thesis: verum