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:87;
then A2: 'not' x is_a_complement_of x by WAYBEL_1:86;
then A3: x "/\" ('not' x) = Bottom L by WAYBEL_1:def 23;
A4: x "\/" ('not' x) = Top L by A2, WAYBEL_1:def 23;
hereby :: thesis: ( y = 'not' x implies y is_a_complement_of x )
assume A5: y is_a_complement_of x ; :: thesis: y = 'not' x
then A6: x "/\" y = Bottom L by WAYBEL_1:def 23;
A7: Top L >= 'not' x by YELLOW_0:45;
A8: Bottom L <= y "/\" ('not' x) by YELLOW_0:44;
Top L >= y by YELLOW_0:45;
then A9: y = (x "\/" ('not' x)) "/\" y by A4, YELLOW_0:25
.= (x "/\" y) "\/" (y "/\" ('not' x)) by WAYBEL_1:def 3
.= y "/\" ('not' x) by A6, A8, YELLOW_0:24 ;
x "\/" y = Top L by A5, WAYBEL_1:def 23;
then 'not' x = (x "\/" y) "/\" ('not' x) by A7, YELLOW_0:25
.= (x "/\" ('not' x)) "\/" (y "/\" ('not' x)) by WAYBEL_1:def 3
.= y "/\" ('not' x) by A3, A8, YELLOW_0:24 ;
hence y = 'not' x by A9; :: thesis: verum
end;
thus ( y = 'not' x implies y is_a_complement_of x ) by A1, WAYBEL_1:86; :: thesis: verum