reconsider F = <%(halt S)%> as Program of ;
( 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 Lm7;
then reconsider F = F as MacroInstruction of S by COMPOS_1:def 14;
take F ; :: thesis: F is really-closed
thus F is really-closed by Th16; :: thesis: verum