Definition. clop_equi
closure_operator H U ↔ set U ∧ map H (power U) (power U) ∧ (∀X. X ⊆ U → X ⊆ app H X) ∧ (∀X. ∀Y. X ⊆ Y → Y ⊆ U → app H X ⊆ app H Y) ∧ (∀X. X ⊆ U → app H (app H X) ⊆ app H X)