I does_not_destroy intloc 0 by SCMFSA7B:def 5;
then Directed I,l does_not_destroy intloc 0 by Th27;
hence Directed I,l is good by SCMFSA7B:def 5; :: thesis: verum