theorem :: RING_2:27

for R being non empty right_unital doubleLoopStr
for a being Element of R holds
( a is irreducible iff <*a*> is_a_factorization_of a ) by fact1;