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

hereby :: thesis: ( ex b being Element of st
( b is-upper-neighbour-of a & ( for c being Element of 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 st
( b is-upper-neighbour-of a & ( for c being Element of st c is-upper-neighbour-of a holds
c = b ) )
then ( a *' is-upper-neighbour-of a & ( for c being Element of st c is-upper-neighbour-of a holds
c = a *' ) ) by Th12;
hence ex b being Element of st
( b is-upper-neighbour-of a & ( for c being Element of st c is-upper-neighbour-of a holds
c = b ) ) ; :: thesis: verum

end;

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

proof

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

end;

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