let L be complete Lattice; :: thesis: for a being Element of L st a is completely-meet-irreducible holds
( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) )
let a be Element of L; :: thesis: ( a is completely-meet-irreducible implies ( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) ) )
assume a is completely-meet-irreducible ; :: thesis: ( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) )
then A1: a *' <> a by Def8;
set X = { x where x is Element of L : ( a [= x & x <> a ) } ;
A2: a [= a *' by Th9;
for c being Element of L st a [= c & c [= a *' & not c = a holds
c = a *'

proof

let c be Element of L; :: thesis: ( a [= c & c [= a *' & not c = a implies c = a *' )
assume A3: ( a [= c & c [= a *' ) ; :: thesis: ( c = a or c = a *' )
assume c <> a ; :: thesis: c = a *'
then c in { x where x is Element of L : ( a [= x & x <> a ) } by A3;
then a *' [= c by LATTICE3:38;
hence c = a *' by A3, LATTICES:26; :: thesis: verum

end;

then A4: for c being Element of L st a [= c & c [= a *' & not c = a *' holds
c = a ;
for c being Element of L st c is-upper-neighbour-of a holds
c = a *'

proof

let c be Element of L; :: thesis: ( c is-upper-neighbour-of a implies c = a *' )
assume A5: c is-upper-neighbour-of a ; :: thesis: c = a *'
then ( a <> c & a [= c & ( for d being Element of L st a [= d & d [= c & not d = c holds
d = a ) ) by Def5;
then c in { x where x is Element of L : ( a [= x & x <> a ) } ;
then ( a [= a *' & a *' [= c ) by Th9, LATTICE3:38;
hence c = a *' by A1, A5, Def5; :: thesis: verum

end;

hence ( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) ) by A1, A2, A4, Def5; :: thesis: verum