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