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 *' ) ) )
set X = { x where x is Element of L : ( a [= x & x <> a ) } ;
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 that
A1: a [= c and
A2: 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 A1;
then a *' [= c by LATTICE3:38;
hence c = a *' by A2, LATTICES:8; :: thesis: verum

end;

then A3: for c being Element of L st a [= c & c [= a *' & not c = 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 A4: a *' <> a ;
A5: 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 A6: c is-upper-neighbour-of a ; :: thesis: c = a *'
then ( a <> c & a [= c ) ;
then c in { x where x is Element of L : ( a [= x & x <> a ) } ;
then A7: a *' [= c by LATTICE3:38;
a [= a *' by Th9;
hence c = a *' by A4, A6, A7; :: thesis: verum

end;

a [= a *' by Th9;
hence ( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) ) by A4, A3, A5; :: thesis: verum