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

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