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