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 normal )
thus ( not id the ordinal non empty number is empty & id the ordinal non empty number is normal ) ; :: thesis: verum