not I destroys intloc 0 by SCMFSA7B:def 5;
then not Directed I destroys intloc 0 by Th6;
hence Directed I is good by SCMFSA7B:def 5; :: thesis: verum