set i = a >0_goto 3;
reconsider Mi = Macro (a >0_goto 3) as good Program of by Th11, SCMFSA7B:13;
if>0 (a,I) = ((Mi ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) ;
hence if>0 (a,I) is good ; :: thesis: verum