Theorem succ_is_set

Proof
01. 1 ⊢ set n, hypo.
02. 1 ⊢ set {n}, set_sg 1.
03. 1 ⊢ set (n ∪ {n}), set_union 1 2.
04. 1 ⊢ set (succ n), eq_subst_rev succ_eq 3, P u ↔ set u.
succ_is_set. ⊢ set n → set (succ n), subj_intro 4.

Dependencies
The given proof depends on six axioms:
comp, eq_refl, eq_subst, ext, pairing, union.