let I be Instruction of SCM+FSA; :: thesis: ( InsCode I <= 8 implies I is Instruction of SCM )
assume A1: InsCode I <= 8 ; :: thesis: I is Instruction of SCM

now :: thesis: not I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} }

assume I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; :: thesis: contradiction
then consider K being Element of Segm 13, dC being Element of SCM+FSA-Data-Loc , fB being Element of SCM+FSA-Data*-Loc such that
A2: I = [K,{},<*dC,fB*>] and
A3: K in {11,12} ;
A4: I `1_3 = K by A2;
( K = 12 or K = 11 ) by A3, TARSKI:def 2;
hence contradiction by A1, A4; :: thesis: verum

end;

then A5: I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } by XBOOLE_0:def 3;

now :: thesis: not I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} }

assume I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dA, dB is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ; :: thesis: contradiction
then consider L being Element of Segm 13, dA, dB being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A6: I = [L,{},<*dB,fA,dA*>] and
A7: L in {9,10} ;
A8: I `1_3 = L by A6;
( L = 9 or L = 10 ) by A7, TARSKI:def 2;
hence contradiction by A1, A8; :: thesis: verum

end;

hence I is Instruction of SCM by A5, XBOOLE_0:def 3; :: thesis: verum