let X be set ; :: thesis: for x, y being Element of (BoolePoset X) holds
( x /\ y in bool X & x \/ y in bool X )
let x, y be Element of (BoolePoset X); :: thesis: ( x /\ y in bool X & x \/ y in bool X )
( x in the carrier of (BoolePoset X) & y in the carrier of (BoolePoset X) ) ;
then A1: ( x in bool X & y in bool X ) by LATTICE3:def 1;
then x /\ y c= X by XBOOLE_1:108;
hence x /\ y in bool X ; :: thesis: x \/ y in bool X
x \/ y c= X by A1, XBOOLE_1:8;
hence x \/ y in bool X ; :: thesis: verum