let T be InsType of SCM-Instr; :: 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
A1: [T,y] in proj1 SCM-Instr by XTUPLE_0:def 12;
consider x being set such that
A2: [[T,y],x] in SCM-Instr by A1, XTUPLE_0:def 12;
reconsider I = [T,y,x] as Element of SCM-Instr by A2;
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 Th10, NAT_1:32; :: thesis: verum