theorem Th25: :: SCMFSA_X:27

for I being really-closed MacroInstruction of SCM+FSA
for k being Nat st k <= card I holds
(Goto k) ";" I is really-closed