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 )

( 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

thus
( not a <= 'not' x implies a <= x )
:: thesis: verum
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;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

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;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