theorem Lm63: :: RINGFRAC:44

for A being domRing holds
( Non_ZeroDiv_Set A = ([#] A) \ {(0. A)} & Non_ZeroDiv_Set A is non empty multiplicatively-closed without_zero Subset of A )