let L be Boolean LATTICE; :: thesis: for a being Element of L holds
( a is atom iff ( a is co-prime & a <> Bottom L ) )
let a be Element of L; :: thesis: ( a is atom iff ( a is co-prime & a <> Bottom L ) )
thus ( a is atom implies ( a is co-prime & a <> Bottom L ) ) :: thesis: ( a is co-prime & a <> Bottom L implies a is atom )

proof

assume A1: a is atom ; :: thesis: ( a is co-prime & a <> Bottom L )

now :: thesis: for x, y being Element of L st a <= x "\/" y & not a <= x holds
a <= y

let x, y be Element of L; :: thesis: ( a <= x "\/" y & not a <= x implies a <= y )
assume that
A2: a <= x "\/" y and
A3: not a <= x ; :: thesis: a <= y
A4: a "/\" x <= a by YELLOW_0:23;
a "/\" x <> a by A3, YELLOW_0:25;
then not Bottom L < a "/\" x by A1, A4;
then A5: ( not Bottom L <= a "/\" x or not Bottom L <> a "/\" x ) by ORDERS_2:def 6;
a = a "/\" (x "\/" y) by A2, YELLOW_0:25
.= (a "/\" x) "\/" (a "/\" y) by WAYBEL_1:def 3
.= a "/\" y by A5, WAYBEL_1:3, YELLOW_0:44 ;
hence a <= y by YELLOW_0:25; :: thesis: verum

end;

hence a is co-prime by WAYBEL14:14; :: thesis: a <> Bottom L
thus a <> Bottom L by A1; :: thesis: verum

end;

assume that
A6: a is co-prime and
A7: a <> Bottom L ; :: thesis: a is atom

A8: now :: thesis: for b being Element of L st Bottom L < b & b <= a holds
b = a

let b be Element of L; :: thesis: ( Bottom L < b & b <= a implies b = a )
assume that
A9: Bottom L < b and
A10: b <= a ; :: thesis: b = a
consider c being Element of L such that
A11: c is_a_complement_of b by WAYBEL_1:def 24;
A12: b "/\" c = Bottom L by A11;
A13: not a <= c by A10, ORDERS_2:3, A9, A12, YELLOW_0:25;
b "\/" c = Top L by A11;
then a <= b "\/" c by YELLOW_0:45;
then a <= b by A6, A13, WAYBEL14:14;
hence b = a by A10, ORDERS_2:2; :: thesis: verum

end;

Bottom L <= a by YELLOW_0:44;
then Bottom L < a by A7, ORDERS_2:def 6;
hence a is atom by A8; :: thesis: verum