let a be Element of R; :: thesis: ( a is irreducible implies a is factorizable )
assume a is irreducible ; :: thesis: a is factorizable
then <*a*> is_a_factorization_of a by fact1;
hence a is factorizable ; :: thesis: verum