Theorem nadd_closed

Proof
01. 1 ⊢ b ∈ ℕ, hypo.
02. 1 ⊢ 0 + b = b, nadd_neutl 1.
03. 1 ⊢ 0 + b ∈ ℕ, eq_subst_rev 2 1, P t ↔ t ∈ ℕ.
04. 4 ⊢ n ∈ ℕ, hypo.
05. 5 ⊢ n + b ∈ ℕ, hypo.
06. 5 ⊢ n + b + 1 ∈ ℕ, succ_in_nat 5.
07. 4 ⊢ n ∈ ℝ, incl_elim nat_incl_in_real 4.
08. 1 ⊢ b ∈ ℝ, incl_elim nat_incl_in_real 1.
09. ⊢ 1 ∈ ℝ, calc.
10. 1, 4 ⊢ n + b + 1 = n + (b + 1), radd_assoc 7 8 9.
11. 1 ⊢ b + 1 = 1 + b, radd_comm 8 9.
12. 1, 4 ⊢ n + b + 1 = n + (1 + b),
  eq_subst 11 10, P t ↔ n + b + 1 = n + t.
13. 1, 4 ⊢ n + 1 + b = n + (1 + b), radd_assoc 7 9 8.
14. 1, 4 ⊢ n + (1 + b) = n + 1 + b, eq_symm 13.
15. 1, 4 ⊢ n + b + 1 = n + 1 + b, eq_trans 12 14.
16. 1, 4, 5 ⊢ n + 1 + b ∈ ℕ, eq_subst 15 6, P t ↔ t ∈ ℕ.
17. 1 ⊢ n ∈ ℕ → n + b ∈ ℕ → n + 1 + b ∈ ℕ, subj_intro_ii 16.
18. 1 ⊢ ∀n. n ∈ ℕ → n + b ∈ ℕ → n + 1 + b ∈ ℕ, uq_intro 17.
19. 1 ⊢ ∀n. n ∈ ℕ → n + b ∈ ℕ,
  nat_induction 3 18, P n ↔ n + b ∈ ℕ.
20. 20 ⊢ a ∈ ℕ, hypo.
21. 20, 1 ⊢ a + b ∈ ℕ, uq_bounded_elim 19 20.
nadd_closed. ⊢ a ∈ ℕ → b ∈ ℕ → a + b ∈ ℕ, subj_intro_ii 21.

Dependencies
The given proof depends on 10 axioms:
comp, eq_refl, eq_subst, ext, radd_assoc, radd_closed, radd_comm, radd_neutr, real_is_set, subset.