( not I destroys intloc 0 & not J destroys intloc 0 ) by SCMFSA7B:def 5;
hence not I +* J destroys intloc 0 by Th4; :: according to SCMFSA7B:def 5 :: thesis: verum