let a2 be Nat; :: thesis: [6,<*a2*>,{}] in SCM-Instr

reconsider x = 6 as Element of Segm 9 by NAT_1:44;

[x,<*a2*>,{}] in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ;

then [x,<*a2*>,{}] in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } by XBOOLE_0:def 3;

then [x,<*a2*>,{}] in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } by XBOOLE_0:def 3;

hence [6,<*a2*>,{}] in SCM-Instr by XBOOLE_0:def 3; :: thesis: verum

reconsider x = 6 as Element of Segm 9 by NAT_1:44;

[x,<*a2*>,{}] in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ;

then [x,<*a2*>,{}] in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } by XBOOLE_0:def 3;

then [x,<*a2*>,{}] in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } by XBOOLE_0:def 3;

hence [6,<*a2*>,{}] in SCM-Instr by XBOOLE_0:def 3; :: thesis: verum