theorem Th7: :: SCMBSORT:8

for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for a being Int-Location
for la being Nat st ic in rng p & ( ic = a =0_goto la or ic = a >0_goto la ) holds
a in UsedILoc p