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