Overspill lemma
= Overspill lemma
{wiki=Overspill}
If a definable property in a <Nonstandard model of Peano arithmetic> holds of every standard natural number, then it holds of some nonstandard element. Equivalently, a definable set containing the entire <standard cut of a nonstandard model of arithmetic> must overspill beyond it.