theorem Th8: :: SCMBSORT:9

for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for fa being FinSeq-Location
for a, b being Int-Location st ic in rng p & ( ic = b := (fa,a) or ic = (fa,a) := b ) holds
( a in UsedILoc p & b in UsedILoc p )