Theorem clop_app_in_cod

Proof
01. 1 ⊢ closure_operator H U, hypo.
02. 2 ⊢ X ⊆ U, hypo.
03. 1 ⊢ set U ∧ map H (power U) (power U),
  lsubj_conj_elimlll clop_equi 1.
04. 1 ⊢ set U, conj_eliml 3.
05. 1 ⊢ map H (power U) (power U), conj_elimr 3.
06. 1, 2 ⊢ set X, subset 2 4.
07. 1, 2 ⊢ X ∈ power U, power_intro 6 2.
08. 1, 2 ⊢ app H X ∈ power U, map_app_in_cod 5 7.
09. 1, 2 ⊢ app H X ⊆ U, power_elim 8.
clop_app_in_cod. ⊢ closure_operator H U → X ⊆ U →
  app H X ⊆ U, subj_intro_ii 9.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.