reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined the InstructionsF of S -valued non empty finite lower Function by Th25;
take F ; :: thesis: ( 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; :: thesis: verum