Theorem transitive_closed_power

Proof
01. 1 ⊢ transitive x, hypo.
02. 2 ⊢ u ∈ power x, hypo.
03. 2 ⊢ u ⊆ x, power_elim 2.
04. 4 ⊢ y ∈ u, hypo.
05. 2, 4 ⊢ y ∈ x, incl_elim 3 4.
06. 1, 2, 4 ⊢ y ⊆ x, transitive_elim 1 5.
07. 4 ⊢ set y, set_intro 4.
08. 1, 2, 4 ⊢ y ∈ power x, power_intro 7 6.
09. 1, 2 ⊢ y ∈ u → y ∈ power x, subj_intro 8.
10. 1, 2 ⊢ ∀y. y ∈ u → y ∈ power x, uq_intro 9.
11. 1, 2 ⊢ u ⊆ power x, incl_intro 10.
12. 1 ⊢ u ∈ power x → u ⊆ power x, subj_intro 11.
13. 1 ⊢ ∀u. u ∈ power x → u ⊆ power x, uq_intro 12.
14. 1 ⊢ transitive (power x), transitive_intro 13.
transitive_closed_power. ⊢ transitive x →
  transitive (power x), subj_intro 14.

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