∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s →
    ∀ {p : Set X → Prop},
      (∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) →
        (∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)) → (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, p t) → p s