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