let L be complete noetherian Lattice; :: thesis: for a being Element of L st a <> Top L holds
( a is completely-meet-irreducible iff a % is meet-irreducible )
let a be Element of L; :: thesis: ( a <> Top L implies ( a is completely-meet-irreducible iff a % is meet-irreducible ) )
assume a <> Top L ; :: thesis: ( a is completely-meet-irreducible iff a % is meet-irreducible )
then consider b being Element of L such that
A1: b is-upper-neighbour-of a by Th6;
A2: b <> a by A1;

now :: thesis: ( a % is meet-irreducible implies a is completely-meet-irreducible )

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

proof

let d be Element of L; :: thesis: ( d is-upper-neighbour-of a implies d = b )
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: d = b
then A7: d <> a ;
assume d <> b ; :: thesis: contradiction
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: verum

end;

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

end;

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