theorem Th30: :: SCMFSA_X:32

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