∀ {α : Type u_1} {c : Cardinal.{u_1}} (l : Set (Set α)),
  (∀ (S : Set (Set α)), Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) →
    ∀ (S : Set (Set α)), Cardinal.mk ↑S < c → S ⊆ {s | sᶜ ∈ l} → ⋂₀ S ∈ {s | sᶜ ∈ l}