let I be Element of SCM+FSA-Instr ; :: thesis: ( InsCode I <= 8 implies I in SCM-Instr )
assume A1: InsCode I <= 8 ; :: thesis: I in SCM-Instr

A2: now

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

end;

A5: now

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

end;

( I in SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } or I in { [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def 3;
hence I in SCM-Instr by A2, A5, XBOOLE_0:def 3; :: thesis: verum