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

hereby :: thesis: ( ex b being Element of L st
( b is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = b ) ) implies a is completely-meet-irreducible )

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

end;

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

proof

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

end;

then b is_less_than { x where x is Element of L : ( a [= x & x <> a ) } by LATTICE3:def 16;
hence a <> a *' by A2, A3, LATTICE3:42; :: according to LATTICE6:def 8 :: thesis: verum