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 )
A1: Irr L c= IRR L by Th22;
assume x is completely-irreducible ; :: thesis: x is meet-irreducible
then x in Irr L by Def4;
hence x is meet-irreducible by A1, WAYBEL_6:def 4; :: thesis: verum