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