:: deftheorem defines without_zero RINGFRAC:def 4 :
for A being non degenerated commutative Ring
for V being Subset of A holds
( V is without_zero iff not 0. A in V );