reconsider F = <%(halt S)%> as NAT -defined the Instructions of S -valued non empty initial FinPartState of ;
take F ; :: thesis: ( F is trivial & F is closed & F is initial & not F is empty )
thus ( F is trivial & F is closed & F is initial & not F is empty ) by Th46; :: thesis: verum