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