thus not the carrier of INT.Ring is finite by INT_3:def 3; :: according to STRUCT_0:def 11 :: thesis: INT.Ring is good
thus the carrier of INT.Ring <> NAT by INT_3:def 3, NUMBERS:27; :: according to SCMRING1:def 2 :: thesis: verum