Theorem int_incl_in_real

Proof
01. ⊢ {z | z ∈ ℝ ∧ ∃a. ∃b. a ∈ ℕ ∧ b ∈ ℕ ∧ z = a - b} ⊆ ℝ,
  sep_is_subclass.
int_incl_in_real. ⊢ ℤ ⊆ ℝ, eq_subst_rev int_eq 1, P t ↔ t ⊆ ℝ.

Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.