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: ( b [= Bottom L & b <> Bottom L ) by A1, Def5;
Bottom L [= b by LATTICES:41;
hence contradiction by A2, LATTICES:26; :: thesis: verum