let L be Semilattice; :: thesis: for x being Element of L st x is completely-irreducible holds
x is meet-irreducible
let x be Element of L; :: thesis: ( x is completely-irreducible implies x is meet-irreducible )
assume x is completely-irreducible ; :: thesis: x is meet-irreducible
then A1: x in Irr L by Def4;
Irr L c= IRR L by Th22;
hence x is meet-irreducible by A1, WAYBEL_6:def 4; :: thesis: verum