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 :: 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 ) ) implies a is completely-join-irreducible )

given b being Element of L such that A2: b is-lower-neighbour-of a and
A3: for c being Element of L st c is-lower-neighbour-of a holds
c = b ; :: thesis: a is completely-join-irreducible
A4: a <> b by A2;
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 q9 being Element of L st
( q9 = q & q9 [= a & q9 <> a ) ;
then ex c being Element of L st
( q [= c & c is-lower-neighbour-of a ) by Th4;
hence q [= b by A3; :: thesis: verum

end;

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

end;

now :: thesis: ( a is completely-join-irreducible implies 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 ) ) )

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;

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