:: deftheorem defines irreducible RING_2:def 9 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is irreducible iff ( x <> 0. R & x is not Unit of R & ( for a being Element of R holds
( not a divides x or a is Unit of R or a is_associated_to x ) ) ) );