自然数の公理から得られる定理だと思います。ちなみに自然数の公理
を違う公理で置き換えると新たな公理体系が得られます。