let T be InsType of SCM; :: thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
consider y being set such that
B1: [T,y] in proj1 the Instructions of SCM by RELAT_1:def 4;
consider x being set such that
A1: [[T,y],x] in the Instructions of SCM by B1, RELAT_1:def 4;
reconsider I = [T,y,x] as Instruction of SCM by A1;
T = InsCode I by RECDEF_2:def 1;
hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) by AMI_5:36, NAT_1:33; :: thesis: verum