theorem Th28: :: SCMFSA_X:30

for I being really-closed MacroInstruction of SCM+FSA
for a being Int-Location
for k being Nat st k <= card I holds
(Macro (a >0_goto k)) ';' I is really-closed