∀ {α : Type u_1} [inst : TopologicalSpace α] {K : Set α} {s : Set (Set α)},
  s ⊆ 𝒫 K →
    ∀ (S : Set (Set (Set α))),
      ∀ L ∈ s,
        L \ ⋃₀ {U | IsOpen U ∧ {s | (s ∩ U).Nonempty} ∈ S} ⊆ K \ ⋃₀ {U | IsOpen U ∧ {s | (s ∩ U).Nonempty} ∈ S} ∩ L