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

end;

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

end;

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