let L be complete co-noetherian Lattice; :: thesis: for a being Element of L holds
( a is completely-join-irreducible iff ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) )
let a be Element of L; :: thesis: ( a is completely-join-irreducible iff ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) )
set X = { x where x is Element of L : ( x [= a & x <> a ) } ;

A1: now

assume a is completely-join-irreducible ; :: thesis: ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) )
then ( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) ) by Th13;
hence ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) ; :: thesis: verum

end;

now

given b being Element of L such that A2: ( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) ; :: thesis: a is completely-join-irreducible
A3: ( b [= a & a <> b ) by A2, Def5;
then A4: b in { x where x is Element of L : ( x [= a & x <> a ) } ;
for q being Element of L st q in { x where x is Element of L : ( x [= a & x <> a ) } holds
q [= b

proof

let q be Element of L; :: thesis: ( q in { x where x is Element of L : ( x [= a & x <> a ) } implies q [= b )
assume q in { x where x is Element of L : ( x [= a & x <> a ) } ; :: thesis: q [= b
then ex q' being Element of L st
( q' = q & q' [= a & q' <> a ) ;
then ex c being Element of L st
( q [= c & c is-lower-neighbour-of a ) by Th4;
hence q [= b by A2; :: thesis: verum

end;

then b is_greater_than { x where x is Element of L : ( x [= a & x <> a ) } by LATTICE3:def 17;
then a <> *' a by A3, A4, LATTICE3:41;
hence a is completely-join-irreducible by Def9; :: thesis: verum

end;

hence ( a is completely-join-irreducible iff ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) ) by A1; :: thesis: verum