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