let L be complete Lattice; :: thesis: for a being Element of L st a is atomic holds
a is completely-join-irreducible
let a be Element of L; :: thesis: ( a is atomic implies a is completely-join-irreducible )
assume a is atomic ; :: thesis: a is completely-join-irreducible
then A1: a is-upper-neighbour-of Bottom L by Def10;
then A2: ( a <> Bottom L & Bottom L [= a & ( for c being Element of L st Bottom L [= c & c [= a & not c = a holds
c = Bottom L ) ) by Def5;
set X = { x where x is Element of L : ( x [= a & x <> a ) } ;
A3: for x being set st x in { x where x is Element of L : ( x [= a & x <> a ) } holds
x in {(Bottom L)}

proof

let x be set ; :: thesis: ( x in { x where x is Element of L : ( x [= a & x <> a ) } implies x in {(Bottom L)} )
assume x in { x where x is Element of L : ( x [= a & x <> a ) } ; :: thesis: x in {(Bottom L)}
then A4: ex x' being Element of L st
( x' = x & x' [= a & x' <> a ) ;
then reconsider x = x as Element of L ;
Bottom L [= x by LATTICES:41;
then x = Bottom L by A1, A4, Def5;
hence x in {(Bottom L)} by TARSKI:def 1; :: thesis: verum

end;

A5: for x being set st x in {(Bottom L)} holds
x in { x where x is Element of L : ( x [= a & x <> a ) }

proof

let x be set ; :: thesis: ( x in {(Bottom L)} implies x in { x where x is Element of L : ( x [= a & x <> a ) } )
assume x in {(Bottom L)} ; :: thesis: x in { x where x is Element of L : ( x [= a & x <> a ) }
then x = Bottom L by TARSKI:def 1;
hence x in { x where x is Element of L : ( x [= a & x <> a ) } by A2; :: thesis: verum

end;

Bottom L = "\/" {(Bottom L)},L by LATTICE3:43
.= *' a by A3, A5, TARSKI:2 ;
hence a is completely-join-irreducible by A2, Def9; :: thesis: verum