Proof 01. 1 ⊢ closure_operator H U, hypo. 02. 1 ⊢ ∀X. ∀Y. X ⊆ Y → Y ⊆ U → app H X ⊆ app H Y, lsubj_conj_elimlr clop_equi 1. 03. 1 ⊢ ∀Y. X ⊆ Y → Y ⊆ U → app H X ⊆ app H Y, uq_elim 2. 04. 1 ⊢ X ⊆ Y → Y ⊆ U → app H X ⊆ app H Y, uq_elim 3. clop_monotony. ⊢ closure_operator H U → X ⊆ Y → Y ⊆ U → app H X ⊆ app H Y, subj_intro 4.