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

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

assume A1: for b being Element of L holds not b is-upper-neighbour-of a ; :: thesis: a = Top 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: a [= c by A2, LATTICES:5;

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
( d [= c & d is-upper-neighbour-of a ) by A3, Th3;
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 = Top L by LATTICES:def 17; :: thesis: verum

end;

hence ( a = Top L iff for b being Element of L holds not b is-upper-neighbour-of a ) by Th5; :: thesis: verum