set i = a >0_goto ((card J) + 3);
reconsider Mi = Macro (a >0_goto ((card J) + 3)) as good Program of SCM+FSA by Th36, SCMFSA7B:19;
if>0 a,I,J = ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 2
.= (((Mi ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ) ;
hence if>0 a,I,J is good ; :: thesis: verum