take Trivial-AMI N ; :: thesis: ( not Trivial-AMI N is empty & Trivial-AMI N is with_non-empty_values )
thus ( not Trivial-AMI N is empty & Trivial-AMI N is with_non-empty_values ) ; :: thesis: verum