∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [BaireSpace X] [Nonempty X] [Countable ι] {f : ι → Set X},
  (∀ (i : ι), IsClosed (f i)) → ⋃ i, f i = Set.univ → ∃ i, (interior (f i)).Nonempty