Description: Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005) (Revised by Mario Carneiro, 25-Jul-2013)