let I be Element of SCM+FSA-Instr ; :: thesis: ( I `1_3 <= 8 implies I in SCM-Instr )
assume A1: I `1_3 <= 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_3 = K by A3, RECDEF_2:def 1;
then ( I `1_3 = 11 or I `1_3 = 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_3 = J by A6, RECDEF_2:def 1;
then ( I `1_3 = 9 or I `1_3 = 10 ) by A7, TARSKI:def 2;
hence contradiction by A1; :: thesis: verum

end;

B5: now

assume I in { [13,{},<*b1*>] where b1 is Element of SCM+FSA-Data-Loc : verum } ; :: thesis: contradiction
then consider b1 being Element of SCM+FSA-Data-Loc such that
A6: I = [13,{},<*b1*>] ;
I `1_3 = 13 by A6, RECDEF_2:def 1;
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} } or I in { [13,{},<*b1*>] where b1 is Element of SCM+FSA-Data-Loc : verum } ) by XBOOLE_0:def 3;
hence I in SCM-Instr by A2, A5, B5, XBOOLE_0:def 3; :: thesis: verum