take Trivial-AMI N ; :: thesis: not Trivial-AMI N is empty
thus not Trivial-AMI N is empty ; :: thesis: verum