Theorem nat_incl_in_real

Proof
let inductive A ↔ A ⊆ ℝ ∧ 0 ∈ A ∧ (∀n. n ∈ A → n + 1 ∈ A).
01. ⊢ ℝ ⊆ ℝ, incl_refl.
02. ⊢ 0 ∈ ℝ, calc.
03. 3 ⊢ n ∈ ℝ, hypo.
04. ⊢ 1 ∈ ℝ, calc.
05. 3 ⊢ n + 1 ∈ ℝ, radd_closed 3 4.
06. ⊢ n ∈ ℝ → n + 1 ∈ ℝ, subj_intro 5.
07. ⊢ ∀n. n ∈ ℝ → n + 1 ∈ ℝ, uq_intro 6.
08. ⊢ ℝ ⊆ ℝ ∧ 0 ∈ ℝ, conj_intro 1 2.
09. ⊢ inductive ℝ, conj_intro 8 7.
10. ⊢ ℝ ∈ {A | inductive A},
  comp_intro real_is_set 9, P A ↔ inductive A.
nat_incl_in_real. ⊢ ℕ ⊆ ℝ, Intersection_is_lower_bound nat_eq 10.

Dependencies
The given proof depends on four axioms:
comp, eq_subst, radd_closed, real_is_set.