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