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

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