Theorem nat_is_set

Proof
nat_is_set. ⊢ set ℕ, subset nat_incl_in_real real_is_set.

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