let cc, aa, bb be Int-Location ; :: thesis: for I, J being Program of SCM+FSA st cc <> aa & not I destroysdestroy cc & not J destroysdestroy cc holds
not if>0 aa,bb,I,J destroysdestroy cc
let I, J be Program of SCM+FSA ; :: thesis: ( cc <> aa & not I destroysdestroy cc & not J destroysdestroy cc implies not if>0 aa,bb,I,J destroysdestroy cc )
assume that
A1: cc <> aa and
A2: ( not I destroysdestroy cc & not J destroysdestroy cc ) ; :: thesis: not if>0 aa,bb,I,J destroysdestroy cc
( if>0 aa,bb,I,J = (SubFrom aa,bb) ';' (if>0 aa,I,J) & not if>0 aa,I,J destroysdestroy cc ) by A2, SCMFSA8B:def 5, SCMFSA8C:121;
hence not if>0 aa,bb,I,J destroysdestroy cc by A1, SCMFSA7B:14, SCMFSA8C:82; :: thesis: verum