theorem :: AMI_3:25

for I being Instruction of SCM st I is halting holds
I = halt SCM by Lm13;