Theorem isub_closed

Proof
01. 1 ⊢ a ∈ ℤ, hypo.
02. 2 ⊢ b ∈ ℤ, hypo.
03. 2 ⊢ -b ∈ ℤ, ineg_closed 2.
04. 1, 2 ⊢ a + (-b) ∈ ℤ, iadd_closed 1 3.
05. ⊢ a - b = a + (-b), rsub_eq.
06. 1, 2 ⊢ a - b ∈ ℤ, eq_subst_rev 5 4, P t ↔ t ∈ ℤ.
isub_closed. ⊢ a ∈ ℤ → b ∈ ℤ → a - b ∈ ℤ, subj_intro_ii 6.

Dependencies
The given proof depends on 16 axioms:
comp, eq_refl, eq_subst, ext, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, real_is_set, rmul_closed, rmul_comm, rmul_distl_add, rmul_neutr, rneg_closed, subset.