theorem Th6: :: SCMFSA8A:13

for I being preProgram of SCM+FSA
for a being Int-Location st not I destroys a holds
not Directed I destroys a