not SubFrom a,b destroysdestroy intloc 0 by SCMFSA7B:14;
hence SubFrom a,b is good by Def6; :: thesis: verum