Theorem truncated_power_closed

Proof
01. 1 ⊢ univ U, hypo.
02. 2 ⊢ x ∈ U, hypo.
03. 1, 2 ⊢ power x ∈ U, univ_closed_power 1 2.
04. ⊢ U ∩ power x ⊆ power x, intersection_incl_right.
05. 1, 2 ⊢ U ∩ power x ∈ U, univ_closed_subset 1 4 3.
truncated_power_closed. ⊢ univ U → x ∈ U → U ∩ power x ∈ U,
  subj_intro_ii 5.

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