theorem Th3: :: RINGFRAC:3

for A being non degenerated commutative Ring holds not 0. A in Non_ZeroDiv_Set A