reconsider A = a as Data-Location by Th5;
reconsider i = A >0_goto la as Instruction of SCM+FSA by Th10;
take i ; :: thesis: ex A being Data-Location st
( a = A & i = A >0_goto la )
take A ; :: thesis: ( a = A & i = A >0_goto la )
thus ( a = A & i = A >0_goto la ) ; :: thesis: verum