take the non empty set --> the ExtNat ; :: thesis: ( not the non empty set --> the ExtNat is empty & the non empty set --> the ExtNat is constant & the non empty set --> the ExtNat is ext-natural-valued )
thus ( not the non empty set --> the ExtNat is empty & the non empty set --> the ExtNat is constant & the non empty set --> the ExtNat is ext-natural-valued ) ; :: thesis: verum