reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined the InstructionsF of S -valued non empty finite lower Function by Th25;
( F . (LastLoc F) = halt S & ( for l being Element of NAT st F . l = halt S & l in dom F holds
l = LastLoc F ) ) by Lm4;
then reconsider F = F as pre-Macro of S by Def12, Def13;
take F ; :: thesis: F is really-closed
thus F is really-closed by Th24; :: thesis: verum