Least-number principle (source code)

= Least-number principle
{wiki=Well-ordering_principle}

Every nonempty definable set of natural numbers has a least element. Over the usual arithmetic language, this principle is equivalent to the induction scheme.