take
Trivial-AMI N
; :: thesis: ( Trivial-AMI N is with_non-empty_values & Trivial-AMI N is 1 -element )

thus ( Trivial-AMI N is with_non-empty_values & Trivial-AMI N is 1 -element ) ; :: thesis: verum

thus ( Trivial-AMI N is with_non-empty_values & Trivial-AMI N is 1 -element ) ; :: thesis: verum