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 & a [= b & ( for c being Element of L st a [= c & c [= b & not c = b holds
c = a ) ) by A1, Def5;

now

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 )
assume A4: d is-upper-neighbour-of a ; :: thesis: d = b
then A5: ( d <> a & a [= d & ( for c being Element of L st a [= c & c [= d & not c = d holds
c = a ) ) by Def5;
assume d <> b ; :: thesis: contradiction
then A6: a = d "/\" b by A1, A4, Th2;
A7: ( a % = a & d % = d & b % = b ) by LATTICE3:def 3;
then a % = (d % ) "/\" (b % ) by A6, Lm8;
hence contradiction by A2, A3, A5, A7, 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