let L be complete noetherian Lattice; :: thesis:
let a be Element of L; :: thesis:
assume a <> Top L ; :: thesis:
then consider b being Element of L such that
A1: b is-upper-neighbour-of a by Th6;
A2: b <> a by A1;

assume A3: a % is meet-irreducible ; :: thesis:
for d being Element of L st d is-upper-neighbour-of a holds
d = b

let d be Element of L; :: thesis:
A4: a % = a by LATTICE3:def 3;
A5: ( d % = d & b % = b ) by LATTICE3:def 3;
assume A6: d is-upper-neighbour-of a ; :: thesis:
then A7: d <> a ;
assume d <> b ; :: thesis:
then a = d "/\" b by A1, A6, Th2;
then a % = (d %) "/\" (b %) by A4, Lm8;
hence contradiction by A2, A3, A7, A4, A5, WAYBEL_6:def 2; :: thesis:

end;

hence a is completely-meet-irreducible by A1, Th14; :: thesis:

end;

hence ( a is completely-meet-irreducible iff a % is meet-irreducible ) by Th16; :: thesis: