let a be Element of R; :: thesis: ( not a is zero & not a is unital implies a is factorizable )
assume ( not a is zero & not a is unital ) ; :: thesis: a is factorizable
then a is uniquely_factorizable by df;
hence a is factorizable ; :: thesis: verum