:: deftheorem defines ZeroDiv_Set RINGFRAC:def 2 :
for A being non degenerated commutative Ring holds ZeroDiv_Set A = { a where a is Element of A : a is Zero_Divisor of A } ;