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

hence I in SCM-Instr by A2, A5, A8, XBOOLE_0:def 3; :: thesis: verum

assume A1: I `1_3 <= 8 ; :: thesis: I in SCM-Instr

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

assume
I in { [K,{},<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM-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-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;

then ( I `1_3 = 11 or I `1_3 = 12 ) by A4, TARSKI:def 2;

hence contradiction by A1; :: thesis: verum

end;then consider K being Element of Segm 13, c being Element of SCM-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;

then ( I `1_3 = 11 or I `1_3 = 12 ) by A4, TARSKI:def 2;

hence contradiction by A1; :: thesis: verum

A5: now :: thesis: not I in { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} }

assume
I in { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} }
; :: thesis: contradiction

then consider J being Element of Segm 13, b, c being Element of SCM-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;

then ( I `1_3 = 9 or I `1_3 = 10 ) by A7, TARSKI:def 2;

hence contradiction by A1; :: thesis: verum

end;then consider J being Element of Segm 13, b, c being Element of SCM-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;

then ( I `1_3 = 9 or I `1_3 = 10 ) by A7, TARSKI:def 2;

hence contradiction by A1; :: thesis: verum

A8: now :: thesis: not I in { [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum }

( I in SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-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-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-Data-Loc : verum } )
by XBOOLE_0:def 3;assume
I in { [13,{},<*b1*>] where b1 is Element of SCM-Data-Loc : verum }
; :: thesis: contradiction

then consider b1 being Element of SCM-Data-Loc such that

A9: I = [13,{},<*b1*>] ;

I `1_3 = 13 by A9;

hence contradiction by A1; :: thesis: verum

end;then consider b1 being Element of SCM-Data-Loc such that

A9: I = [13,{},<*b1*>] ;

I `1_3 = 13 by A9;

hence contradiction by A1; :: thesis: verum

hence I in SCM-Instr by A2, A5, A8, XBOOLE_0:def 3; :: thesis: verum