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