for L being noetherian Lattice
for a, d being Element of L st a [= d & a <> d holds
ex c being Element of L st
( c [= d & c is-upper-neighbour-of a )