reconsider F = (il. S,0 ) .--> (halt S) as NAT -defined non empty lower FinPartState of S by Th48;
( F is halt-ending & F is unique-halt )

proof

thus ( F . (LastLoc F) = halt S & ( for l being Instruction-Location of S st F . l = halt S & l in dom F holds
l = LastLoc F ) ) by Lm7; :: according to AMISTD_1:def 22,AMISTD_1:def 23 :: thesis: verum

end;

then reconsider F = F as pre-Macro of S ;
take F ; :: thesis: F is closed
thus F is closed by Th46; :: thesis: verum