:: deftheorem df defines factorial RING_2:def 15 :
for R being non degenerated Ring holds
( R is factorial iff for a being non zero Element of R st a is NonUnit of R holds
a is uniquely_factorizable );