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 Th2;
reconsider b = X \ a as Element of (BoolePoset X) by Th2;
A2: a misses b by XBOOLE_1:79;
A3: a "/\" b = a /\ b by YELLOW_1:17
.= {} by A2
.= Bottom (BoolePoset X) by YELLOW_1:18 ;
a "\/" b = a \/ b by YELLOW_1:17
.= X by A1, XBOOLE_1:45
.= Top (BoolePoset X) by YELLOW_1:19 ;
then b is_a_complement_of a by A3, WAYBEL_1:def 23;
hence 'not' a = X \ a by YELLOW_5:11; :: thesis: verum