theorem :: RING_4:34

for R being domRing holds
( R is Field iff for a being NonUnit of R holds a = 0. R ) by lemf;