reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined non empty lower FinPartState of by Th48;
( 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 pre-Macro of S by Def22, Def23;
take F ; :: thesis: F is closed
thus F is closed by Th46; :: thesis: verum