Theorem nat_induction_sets

Proof
let inductive A ↔ A ⊆ ℝ ∧ 0 ∈ A ∧ (∀n. n ∈ A → n + 1 ∈ A).
01. 1 ⊢ A ⊆ ℕ, hypo.
02. 2 ⊢ 0 ∈ A, hypo.
03. 3 ⊢ ∀n. n ∈ A → n + 1 ∈ A, hypo.
04. 1 ⊢ A ⊆ ℝ, incl_trans 1 nat_incl_in_real.
05. 1, 2 ⊢ A ⊆ ℝ ∧ 0 ∈ A, conj_intro 4 2.
06. 1, 2, 3 ⊢ inductive A, conj_intro 5 3.
07. 1 ⊢ set A, subset 1 nat_is_set.
08. 1, 2, 3 ⊢ A ∈ {A | inductive A}, comp_intro 7 6.
09. 1, 2, 3 ⊢ ℕ ⊆ A, Intersection_is_lower_bound nat_eq 8.
10. 1, 2, 3 ⊢ A = ℕ, incl_antisym 1 9.
nat_induction_sets. ⊢ A ⊆ ℕ → 0 ∈ A →
  (∀n. n ∈ A → n + 1 ∈ A) → A = ℕ, subj_intro_iii 10.

Dependencies
The given proof depends on six axioms:
comp, eq_subst, ext, radd_closed, real_is_set, subset.