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 ;
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
.= (a "/\" x) "\/" (a "/\" y) by WAYBEL_1:def 3
.= a "/\" y by ;
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 ;
b "\/" c = Top L by A11;
then a <= b "\/" c by YELLOW_0:45;
then a <= b by ;
hence b = a by ; :: thesis: verum
end;
Bottom L <= a by YELLOW_0:44;
then Bottom L < a by ;
hence a is atom by A8; :: thesis: verum