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