theorem :: SCMFSA8C:47

for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
not Directed I destroys a by SCMFSA8A:13;