set A = the non empty Ordinal;
take id the non empty Ordinal ; :: thesis: ( not id the non empty Ordinal is empty & id the non empty Ordinal is increasing & id the non empty Ordinal is continuous )
thus ( not id the non empty Ordinal is empty & id the non empty Ordinal is increasing & id the non empty Ordinal is continuous ) ; :: thesis: verum