let L be complete Lattice; :: thesis: for a being Element of L st a is completely-join-irreducible holds
( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) )
let a be Element of L; :: thesis: ( a is completely-join-irreducible implies ( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) ) )
assume a is completely-join-irreducible ; :: thesis: ( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) )
then A1: *' a <> a by Def9;
set X = { x where x is Element of L : ( x [= a & x <> a ) } ;
A2: *' a [= a by Th9;
A3: 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 A4: ( *' 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 : ( x [= a & x <> a ) } by A4;
then c [= *' a by LATTICE3:38;
hence c = *' a by A4, LATTICES:26; :: thesis: verum

end;

for c being Element of L st c is-lower-neighbour-of a holds
c = *' a

proof

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

end;

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