theorem Th2: :: SCMFSA8A:9

for P being preProgram of SCM+FSA
for n being Element of NAT
for a being Int-Location st not P destroys a holds
not Reloc (P,n) destroys a