let L be Boolean LATTICE; :: thesis: for x, a being Element of L st a is atom holds
( a <= x iff not a <= 'not' x )
let x, a be Element of L; :: thesis: ( a is atom implies ( a <= x iff not a <= 'not' x ) )
assume A1: a is atom ; :: thesis: ( a <= x iff not a <= 'not' x )
thus ( a <= x implies not a <= 'not' x ) :: thesis: ( not a <= 'not' x implies a <= x )

proof

assume that
A2: a <= x and
A3: a <= 'not' x ; :: thesis: contradiction
a = a "\/" (Bottom L) by WAYBEL_1:3
.= a "\/" (x "/\" ('not' x)) by YELLOW_5:34
.= (a "\/" x) "/\" (('not' x) "\/" a) by WAYBEL_1:5
.= x "/\" (('not' x) "\/" a) by A2, YELLOW_0:24
.= x "/\" ('not' x) by A3, YELLOW_0:24
.= Bottom L by YELLOW_5:34 ;
hence contradiction by A1; :: thesis: verum

end;

thus ( not a <= 'not' x implies a <= x ) :: thesis: verum

proof

a <= Top L by YELLOW_0:45;
then A4: a <= x "\/" ('not' x) by YELLOW_5:34;
assume ( not a <= 'not' x & not a <= x ) ; :: thesis: contradiction
hence contradiction by A1, A4, WAYBEL14:14; :: thesis: verum

end;