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: not the carrier of INT.Ring = SCM-Instr INT.Ring
assume the carrier of INT.Ring = SCM-Instr INT.Ring ; :: thesis: contradiction
then X: 1 in SCM-Instr INT.Ring by INT_1:def 2, INT_3:def 3;
W: SCM-Instr INT.Ring c= [:NAT ,(proj2 (SCM-Instr INT.Ring )):] by SCMRING1:21;
1 in [:NAT ,(proj2 (SCM-Instr INT.Ring )):] by W, X;
then ex a, b being set st
( a in NAT & b in proj2 (SCM-Instr INT.Ring ) & 1 = [a,b] ) by ZFMISC_1:def 2;
hence contradiction ; :: thesis: verum