not I destroys intloc 0 by SCMFSA7B:def 5;
then not Directed (I,l) destroys intloc 0 by Th27;
hence Directed (I,l) is good by SCMFSA7B:def 5; :: thesis: verum