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

proof

a [= a *' by Th9;
then A2: a % <= (a *') % by LATTICE3:7;
A3: % (a %) = a % by LATTICE3:def 4;
A4: ( a = a % & a *' = (a *') % ) by LATTICE3:def 3;
A5: a *' is_less_than { d where d is Element of L : ( a [= d & d <> a ) } by LATTICE3:34;
let x, y be Element of (LattPOSet L); :: thesis: ( not a % = x "/\" y or x = a % or y = a % )
A6: a = a % by LATTICE3:def 3
.= % (a %) by LATTICE3:def 4 ;
A7: x = % x by LATTICE3:def 4
.= (% x) % by LATTICE3:def 3 ;
assume A8: a % = x "/\" y ; :: thesis: ( x = a % or y = a % )
then a % <= x by YELLOW_0:23;
then A9: a [= % x by A7, LATTICE3:7;
assume that
A10: x <> a % and
A11: y <> a % ; :: thesis: contradiction
A12: y = % y by LATTICE3:def 4
.= (% y) % by LATTICE3:def 3 ;
a % <= y by A8, YELLOW_0:23;
then A13: a [= % y by A12, LATTICE3:7;
y = % y by LATTICE3:def 4;
then % y in { d where d is Element of L : ( a [= d & d <> a ) } by A6, A13, A3, A11;
then a *' [= % y by A5, LATTICE3:def 16;
then A14: (a *') % <= (% y) % by LATTICE3:7;
x = % x by LATTICE3:def 4;
then % x in { d where d is Element of L : ( a [= d & d <> a ) } by A6, A9, A3, A10;
then a *' [= % x by A5, LATTICE3:def 16;
then (a *') % <= (% x) % by LATTICE3:7;
then (a *') % <= a % by A8, A12, A7, A14, YELLOW_0:23;
hence contradiction by A1, A2, A4, ORDERS_2:2; :: thesis: verum

end;

hence a % is meet-irreducible by WAYBEL_6:def 2; :: thesis: verum