:: deftheorem Def1 defines zero_divisible RINGFRAC:def 1 :
for R being commutative Ring
for r being Element of R holds
( r is zero_divisible iff ex r1 being Element of R st
( r1 <> 0. R & r * r1 = 0. R ) );