let X be set ; :: thesis: for a being Element of (BoolePoset X) holds 'not' a = X \ a
let a be Element of (BoolePoset X); :: thesis: 'not' a = X \ a
A1: the carrier of (BoolePoset X) = bool X by Th4;
reconsider b = X \ a as Element of (BoolePoset X) by Th4;
b is_a_complement_of a

proof

thus a "\/" b = a \/ b by YELLOW_1:17
.= X by A1, XBOOLE_1:45
.= Top (BoolePoset X) by YELLOW_1:19 ; :: according to WAYBEL_1:def 23 :: thesis: a "/\" b = Bottom (BoolePoset X)
A2: a misses b by XBOOLE_1:79;
thus a "/\" b = a /\ b by YELLOW_1:17
.= {} by A2, XBOOLE_0:def 7
.= Bottom (BoolePoset X) by YELLOW_1:18 ; :: thesis: verum

end;

hence 'not' a = X \ a by YELLOW_5:11; :: thesis: verum