let ins be Instruction of SCM; :: thesis: ( InsCode ins = 8 implies ex loc being Element of NAT ex da being Data-Location st ins = da >0_goto loc )
assume A1: InsCode ins = 8 ; :: thesis: ex loc being Element of NAT ex da being Data-Location st ins = da >0_goto loc

A2: now

assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; :: thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{}] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def 1; :: thesis: verum

end;

now

assume ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ; :: thesis: contradiction
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A3: ins = [I,{},<*b,c*>] and
A4: I in {1,2,3,4,5} ;
InsCode ins = I by A3, RECDEF_2:def 1;
hence contradiction by A1, A4, ENUMSET1:def 3; :: thesis: verum

end;

then A5: ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by AMI_3:27, XBOOLE_0:def 3;
not ins in {[SCM-Halt,{},{}]} by A1, Th37, AMI_3:26, TARSKI:def 1;
then not ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, XBOOLE_0:def 3;
then ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by A5, XBOOLE_0:def 3;
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of Data-Locations such that
A6: ins = [K,<*a1*>,<*b1*>] and
K in {7,8} ;
reconsider da = b1 as Data-Location by Lm1;
reconsider loc = a1 as Element of NAT ;
take loc ; :: thesis: ex da being Data-Location st ins = da >0_goto loc
take da ; :: thesis: ins = da >0_goto loc
thus ins = da >0_goto loc by A1, A6, RECDEF_2:def 1; :: thesis: verum