let x be Element of (BoolePoset X); :: according to WAYBEL_1:def 24 :: thesis: ex y being Element of (BoolePoset X) st y is_a_complement_of x
A1: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def 2
.= bool X by LATTICE3:def 1 ;
then reconsider y = X \ x as Element of (BoolePoset X) by XBOOLE_1:109;
take y ; :: thesis: y is_a_complement_of x
thus x "\/" y = x \/ y by YELLOW_1:17
.= X \/ x by XBOOLE_1:39
.= X by A1, XBOOLE_1:12
.= Top (BoolePoset X) by YELLOW_1:19 ; :: according to WAYBEL_1:def 23 :: thesis: x "/\" y = Bottom (BoolePoset X)
A2: x misses y by XBOOLE_1:79;
thus x "/\" y = x /\ y by YELLOW_1:17
.= {} by A2
.= Bottom (BoolePoset X) by YELLOW_1:18 ; :: thesis: verum