take Trivial-AMI IL,N ; :: thesis: Trivial-AMI IL,N is halting
thus Trivial-AMI IL,N is halting ; :: thesis: verum