Proof 01. 1 ⊢ closure_operator H U, hypo. 02. 2 ⊢ X ⊆ U, hypo. 03. 1 ⊢ ∀X. X ⊆ U → X ⊆ app H X, lsubj_conj_elimllr clop_equi 1. 04. 1, 2 ⊢ X ⊆ app H X, uq_bounded_elim 3 2. clop_extensivity. ⊢ closure_operator H U → X ⊆ U → X ⊆ app H X, subj_intro_ii 4.