theorem Th64: :: RINGFRAC:45

for A being domRing
for a being Element of A holds
( a in Non_ZeroDiv_Set A iff a <> 0. A )