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 by A1;

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

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 )
A4: a % = a by LATTICE3:def 3;
A5: ( d % = d & b % = b ) by LATTICE3:def 3;
assume A6: d is-lower-neighbour-of a ; :: thesis: d = b
then A7: a <> d ;
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 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