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