theorem Th20: :: SFMASTR3:22

for aa, bb, cc being Int-Location
for I being MacroInstruction of SCM+FSA holds {aa,bb,cc} \/ (UsedILoc I) c= UsedILoc (for-up (aa,bb,cc,I))