Theorem nadd_comm

Proof
nadd_comm. ⊢ a ∈ ℕ → b ∈ ℕ → a + b = b + a,
  pred_ii_restr nat_incl_in_real radd_comm.

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