:: deftheorem defprim defines prime RING_2:def 8 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is prime iff ( x <> 0. R & x is not Unit of R & ( for a, b being Element of R holds
( not x divides a * b or x divides a or x divides b ) ) ) );