:: deftheorem defines is-upper-neighbour-of LATTICE6:def 5 :
for L being Lattice
for a, b being Element of L holds
( a is-upper-neighbour-of b iff ( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds
c = b ) ) );