reconsider IG = I ';' (goto 0) as really-closed MacroInstruction of SCM+FSA by Th23;
reconsider W = if>0 (a,IG) as really-closed MacroInstruction of SCM+FSA ;
card W = (card (I ';' (goto 0))) + 4 by Th2
.= ((card I) + 1) + 4 by COMPOS_2:11
.= (card I) + 5 ;
then A2: (card I) + 2 < card W by XREAL_1:8;
W +* (((card I) + 2),(goto 0)) is really-closed by Th22, A2;
hence while>0 (a,I) is really-closed ; :: thesis: verum