let L be lower-bounded co-noetherian Lattice; :: thesis: for a being Element of L holds
( a = Bottom L iff for b being Element of L holds not b is-lower-neighbour-of a )
let a be Element of L; :: thesis: ( a = Bottom L iff for b being Element of L holds not b is-lower-neighbour-of a )

now :: thesis: ( ( for b being Element of L holds not b is-lower-neighbour-of a ) implies a = Bottom L )

assume A1: for b being Element of L holds not b is-lower-neighbour-of a ; :: thesis: a = Bottom L
for b being Element of L holds
( a "/\" b = a & b "/\" a = a )

proof

let b be Element of L; :: thesis: ( a "/\" b = a & b "/\" a = a )
consider c being Element of L such that
A2: c = a "/\" b ;
A3: c [= a by A2, LATTICES:6;

per cases ( a <> c or a = c ) ;

suppose a <> c ; :: thesis: ( a "/\" b = a & b "/\" a = a )

then ex d being Element of L st
( c [= d & d is-lower-neighbour-of a ) by A3, Th4;
hence ( a "/\" b = a & b "/\" a = a ) by A1; :: thesis: verum

end;

suppose a = c ; :: thesis: ( a "/\" b = a & b "/\" a = a )

hence ( a "/\" b = a & b "/\" a = a ) by A2; :: thesis: verum

end;

end;

end;

hence a = Bottom L by LATTICES:def 16; :: thesis: verum

end;

hence ( a = Bottom L iff for b being Element of L holds not b is-lower-neighbour-of a ) by Th7; :: thesis: verum