let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for k being Nat st k <= card I holds
(Goto k) ";" I is really-closed
let k be Nat; :: thesis: ( k <= card I implies (Goto k) ";" I is really-closed )
(Goto k) ";" I = (Macro (goto k)) ';' I by SCMFSA8A:43;
hence ( k <= card I implies (Goto k) ";" I is really-closed ) by Th24; :: thesis: verum