let T be InsType of the InstructionsF of SCM; :: thesis: not not T = 0 & ... & not T = 8
consider y being object such that
A1: [T,y] in proj1 the InstructionsF of SCM by XTUPLE_0:def 12;
consider x being object such that
A2: [[T,y],x] in the InstructionsF of SCM by A1, XTUPLE_0:def 12;
reconsider I = [T,y,x] as Instruction of SCM by A2;
T = InsCode I ;
hence not not T = 0 & ... & not T = 8 by AMI_5:5; :: thesis: verum