:: deftheorem defines Non_ZeroDiv_Set RINGFRAC:def 3 :
for A being non degenerated commutative Ring holds Non_ZeroDiv_Set A = ([#] A) \ (ZeroDiv_Set A);