let L be complete co-noetherian Lattice; :: thesis: for a being Element of L st a <> Bottom L holds
( a is completely-join-irreducible iff a % is join-irreducible )
let a be Element of L; :: thesis: ( a <> Bottom L implies ( a is completely-join-irreducible iff a % is join-irreducible ) )
assume a <> Bottom L ; :: thesis: ( a is completely-join-irreducible iff a % is join-irreducible )
then consider b being Element of L such that
A1: b is-lower-neighbour-of a by Th8;
A2: ( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds
c = b ) ) by A1, Def5;

now

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

proof

let d be Element of L; :: thesis: ( d is-lower-neighbour-of a implies d = b )
assume A4: d is-lower-neighbour-of a ; :: thesis: d = b
then A5: ( a <> d & d [= a & ( for c being Element of L st d [= c & c [= a & not c = a holds
c = d ) ) 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 3; :: thesis: verum

end;

hence a is completely-join-irreducible by A1, Th15; :: thesis: verum

end;

hence ( a is completely-join-irreducible iff a % is join-irreducible ) by Th18; :: thesis: verum