reconsider F = <%(halt S)%> as NAT -defined the Instructions of S -valued non empty initial FinPartState of ;
take F ; :: thesis: ( F is halt-ending & F is unique-halt & F is trivial & F is closed )
thus F . (LastLoc F) = halt S by Lm7; :: according to COMPOS_1:def 25 :: thesis: ( F is unique-halt & F is trivial & F is closed )
thus for f being Element of NAT st F . f = halt S & f in dom F holds
f = LastLoc F by Lm7; :: according to COMPOS_1:def 26 :: thesis: ( F is trivial & F is closed )
thus ( F is trivial & F is closed ) by Th46; :: thesis: verum