theorem Th2: :: RINGFRAC:2

for A being non degenerated commutative Ring holds 1. A is not Zero_Divisor of A