theorem Th7: :: SFMASTR3:9

for aa, bb, cc being Int-Location
for I, J being really-closed MacroInstruction of SCM+FSA st cc <> aa & not I destroys cc & not J destroys cc holds
not if>0 (aa,bb,I,J) destroys cc