theorem Th8: :: LATTICE6:8

for L being lower-bounded co-noetherian Lattice
for a being Element of L holds
( a = Bottom L iff for b being Element of L holds not b is-lower-neighbour-of a )