take idseq n ; :: thesis: ( idseq n is increasing & idseq n is positive-yielding & idseq n is n -element )
thus ( idseq n is increasing & idseq n is positive-yielding & idseq n is n -element ) ; :: thesis: verum