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 )

A6: a is co-prime and

A7: a <> Bottom L ; :: thesis: a is atom

then Bottom L < a by A7, ORDERS_2:def 6;

hence a is atom by A8; :: thesis: verum

( 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 that
assume A1:
a is atom
; :: thesis: ( a is co-prime & a <> Bottom L )

thus a <> Bottom L by A1; :: thesis: verum

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

a <= y

hence
a is co-prime
by WAYBEL14:14; :: thesis: a <> Bottom La <= 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;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

thus a <> Bottom L by A1; :: thesis: verum

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

Bottom L <= a
by YELLOW_0:44;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;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

then Bottom L < a by A7, ORDERS_2:def 6;

hence a is atom by A8; :: thesis: verum