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 )
set X = { x where x is Element of L : ( x [= a & x <> a ) } ;
assume a is atomic ; :: thesis: a is completely-join-irreducible
then A1: a is-upper-neighbour-of Bottom L ;
then A2: a <> Bottom L ;
A3: for x being object st x in { x where x is Element of L : ( x [= a & x <> a ) } holds
x in {(Bottom L)}

proof

let x be object ; :: 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 x9 being Element of L st
( x9 = x & x9 [= a & x9 <> a ) ;
then reconsider x = x as Element of L ;
Bottom L [= x by LATTICES:16;
then x = Bottom L by A1, A4;
hence x in {(Bottom L)} by TARSKI:def 1; :: thesis: verum

end;

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

proof

let x be object ; :: 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, A5; :: thesis: verum

end;

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