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 and
A2: for c being Element of L st c is-upper-neighbour-of a holds
c = b ; :: thesis: a is completely-meet-irreducible
A3: a <> b by A1;
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 q9 being Element of L st
( q9 = q & a [= q9 & q9 <> a ) ;
then ex c being Element of L 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 L : ( a [= x & x <> a ) } by LATTICE3:def 16;
a [= b by A1;
then b in { x where x is Element of L : ( a [= x & x <> a ) } by A3;
hence a <> a *' by A3, A4, LATTICE3:41; :: according to LATTICE6:def 8 :: thesis: verum