Inductive set (source code)

= Inductive set
{title2=$\varnothing\in I\ \land\ \forall x\in I\ (x\cup\{x\}\in I)$}

A <set> $I$ is inductive if it contains the <empty set> and contains $x\cup\{x\}$ whenever it contains $x$. The <axiom of infinity> asserts that an <inductive set> exists. The <natural numbers> form the least <inductive set>: intersect one <inductive set> with the class of objects belonging to every <inductive set>. This use of <separation> gives a <set>, and the defining class is closed under successor.