let L be upper-bounded Lattice; :: thesis: for b being Element of L holds not b is-upper-neighbour-of Top L
given b being Element of L such that A1: b is-upper-neighbour-of Top L ; :: thesis: contradiction
A2: b [= Top L by LATTICES:19;
( Top L [= b & Top L <> b ) by A1;
hence contradiction by A2, LATTICES:8; :: thesis: verum