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