theorem Th24: :: SCMFSA_X:26

for I being really-closed Program of
for k being Nat st k <= card I holds
(Macro (goto k)) ';' I is really-closed