Theorem power_UnivCl

Proof
01. 1 ⊢ x ∈ UnivCl, hypo.
02. 1 ⊢ set x, set_intro 1.
03. ⊢ x ⊆ UnivCl, UnivCl_is_greatest.
04. 1 ⊢ x ∈ power UnivCl, power_intro 2 3.
05. ⊢ x ∈ UnivCl → x ∈ power UnivCl, subj_intro 4.
06. ⊢ ∀x. x ∈ UnivCl → x ∈ power UnivCl, uq_intro 5.
07. ⊢ UnivCl ⊆ power UnivCl, incl_intro 6.
08. ⊢ power UnivCl ⊆ UnivCl, UnivCl_is_greatest.
power_UnivCl. ⊢ power UnivCl = UnivCl, incl_antisym 8 7.

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