:: deftheorem defines IRR RING_2:def 10 :
for R being non empty right_unital doubleLoopStr holds IRR R = { x where x is Element of R : x is irreducible } ;