reconsider F = <%(halt S)%> as NAT -defined non empty initial FinPartState 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 pre-Macro of S by COMPOS_1:def 25, COMPOS_1:def 26;
take F ; :: thesis: F is closed
thus F is closed by Th46; :: thesis: verum