Definition. closure_system_equi
closure_system M U ↔ M ⊆ power U ∧ U ∈ M ∧ ∀T. T ⊆ M → ¬T=∅ → ⋂T ∈ M