reconsider F = (il. S,0 ) .--> (halt S) as NAT -defined non empty lower FinPartState of S by Th48;
take F ; :: thesis: ( F is trivial & F is closed & F is lower & not F is empty )
thus ( F is trivial & F is closed & F is lower & not F is empty ) by Th46; :: thesis: verum