let T be InsType of SCM-Instr; :: thesis: not not T = 0 & ... & not T = 8
consider y being object such that
A1: [T,y] in proj1 SCM-Instr by XTUPLE_0:def 12;
consider x being object 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 ;
hence not not T = 0 & ... & not T = 8 by Th10, NAT_1:60; :: thesis: verum