theorem Th6: :: LATTICE6:6

for L being upper-bounded noetherian Lattice
for a being Element of L holds
( a = Top L iff for b being Element of L holds not b is-upper-neighbour-of a )