reconsider A = a as Data-Location by Th25;
la in NAT by AMI_1:def 4;
then reconsider L = la as Instruction-Location of SCM by AMI_1:def 4;
reconsider i = A >0_goto L as Instruction of by Th38;
take i ; :: thesis: ex A being Data-Location ex La being Instruction-Location of SCM st
( a = A & la = La & i = A >0_goto La )
take A ; :: thesis: ex La being Instruction-Location of SCM st
( a = A & la = La & i = A >0_goto La )
take L ; :: thesis: ( a = A & la = L & i = A >0_goto L )
thus ( a = A & la = L & i = A >0_goto L ) ; :: thesis: verum