let L be Boolean LATTICE; :: thesis: for x, y being Element of L holds
( y is_a_complement_of x iff y = 'not' x )
let x, y be Element of L; :: thesis: ( y is_a_complement_of x iff y = 'not' x )
A1: for x being Element of L holds 'not' ('not' x) = x by WAYBEL_1:90;
then 'not' x is_a_complement_of x by WAYBEL_1:89;
then A2: ( x "\/" ('not' x) = Top L & x "/\" ('not' x) = Bottom L ) by WAYBEL_1:def 23;

hereby :: thesis: ( y = 'not' x implies y is_a_complement_of x )

assume y is_a_complement_of x ; :: thesis: y = 'not' x
then A3: ( x "\/" y = Top L & x "/\" y = Bottom L ) by WAYBEL_1:def 23;
A4: Bottom L <= y "/\" ('not' x) by YELLOW_0:44;
Top L >= 'not' x by YELLOW_0:45;
then A5: 'not' x = (x "\/" y) "/\" ('not' x) by A3, YELLOW_0:25
.= (x "/\" ('not' x)) "\/" (y "/\" ('not' x)) by WAYBEL_1:def 3
.= y "/\" ('not' x) by A2, A4, YELLOW_0:24 ;
Top L >= y by YELLOW_0:45;
then y = (x "\/" ('not' x)) "/\" y by A2, YELLOW_0:25
.= (x "/\" y) "\/" (y "/\" ('not' x)) by WAYBEL_1:def 3
.= y "/\" ('not' x) by A3, A4, YELLOW_0:24 ;
hence y = 'not' x by A5; :: thesis: verum

end;

thus ( y = 'not' x implies y is_a_complement_of x ) by A1, WAYBEL_1:89; :: thesis: verum