theorem Th2: :: LATTICE3:2

for X being set
for x, y being Element of (BooleLatt X) holds
( x [= y iff x c= y ) by XBOOLE_1:7, XBOOLE_1:12;