let L be complete Lattice; :: thesis: for a being Element of L st a is completely-join-irreducible holds
a % is join-irreducible
let a be Element of L; :: thesis: ( a is completely-join-irreducible implies a % is join-irreducible )
set X = { d where d is Element of L : ( d [= a & d <> a ) } ;
assume a is completely-join-irreducible ; :: thesis: a % is join-irreducible
then A1: a <> *' a by Def9;
for x, y being Element of (LattPOSet L) holds
( not a % = x "\/" y or x = a % or y = a % )

proof

let x, y be Element of (LattPOSet L); :: thesis: ( not a % = x "\/" y or x = a % or y = a % )
assume A2: a % = x "\/" y ; :: thesis: ( x = a % or y = a % )
then A3: ( x <= a % & y <= a % & ( for d being Element of (LattPOSet L) st d >= x & d >= y holds
a % <= d ) ) by YELLOW_0:22;
A4: a = a % by LATTICE3:def 3
.= % (a % ) by LATTICE3:def 4 ;
A5: y = % y by LATTICE3:def 4
.= (% y) % by LATTICE3:def 3 ;
A6: x = % x by LATTICE3:def 4
.= (% x) % by LATTICE3:def 3 ;
then A7: ( % x [= a & % y [= a ) by A3, A5, LATTICE3:7;
A8: ( x = % x & y = % y & % (a % ) = a % ) by LATTICE3:def 4;
A9: *' a [= a by Th9;
assume ( x <> a % & y <> a % ) ; :: thesis: contradiction
then A10: ( % x in { d where d is Element of L : ( d [= a & d <> a ) } & % y in { d where d is Element of L : ( d [= a & d <> a ) } ) by A4, A7, A8;
( { d where d is Element of L : ( d [= a & d <> a ) } is_less_than *' a & ( for b being Element of L st { d where d is Element of L : ( d [= a & d <> a ) } is_less_than b holds
*' a [= b ) ) by LATTICE3:def 21;
then ( % x [= *' a & % y [= *' a ) by A10, LATTICE3:def 17;
then ( (*' a) % >= x & (*' a) % >= y ) by A5, A6, LATTICE3:7;
then A11: (*' a) % >= a % by A2, YELLOW_0:22;
A12: a % >= (*' a) % by A9, LATTICE3:7;
( a = a % & *' a = (*' a) % ) by LATTICE3:def 3;
hence contradiction by A1, A11, A12, ORDERS_2:25; :: thesis: verum

end;

hence a % is join-irreducible by WAYBEL_6:def 3; :: thesis: verum