Theorem 1.8.1.40 (Induction principle).  Let M ⊆ . Then the following are equivalent:
  1. 0 ∈ M and ∀ m ∈ M : m + 1 ∈ M
  2. ∀ n ∈  s.t. <n ⊆ M : n ∈ M
  3. M = 
Proof.
Remarks.

Structural induction on the natural numbers is a direct consequence of their definition as a construction. This set-theoretic form of the induction principle is provable from it.

References.