∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] [Nonempty ι] {V : ι → Set X},
  Directed (fun x1 x2 => x1 ⊇ x2) V →
    (∀ (i : ι), IsClosed (V i)) → ∀ {U : Set X}, (∀ x ∈ ⋂ i, V i, U ∈ nhds x) → ∃ i, V i ⊆ U