for L being Lattice
for a, b, c being Element of L st b <> c holds
( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )