let a be Int-Location ; :: thesis: for il being Element of NAT holds a >0_goto il = [8,<*il*>,<*a*>]
let il be Element of NAT ; :: thesis: a >0_goto il = [8,<*il*>,<*a*>]
ex A being Data-Location st
( A = a & A >0_goto il = a >0_goto il ) by SCMFSA_2:def 15;
hence a >0_goto il = [8,<*il*>,<*a*>] ; :: thesis: verum