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) ;
then A1: x 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
y in the carrier of (BoolePoset X) ;
then y in bool X by LATTICE3:def 1;
then x \/ y c= X by A1, XBOOLE_1:8;
hence x \/ y in bool X ; :: thesis: verum