reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined the InstructionsF of S -valued non empty finite lower Function by Th25;
take
F
; ( F is trivial & F is really-closed & F is lower & not F is empty )
thus
( F is trivial & F is really-closed & F is lower & not F is empty )
by Th24; verum