∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} {l : Filter X}
  (motive : (∃ x ∈ s, ClusterPt x (l ⊓ Filter.principal s)) → Prop) (x : ∃ x ∈ s, ClusterPt x (l ⊓ Filter.principal s)),
  (∀ (a : X) (has : a ∈ s) (ha : ClusterPt a (l ⊓ Filter.principal s)), motive ⋯) → motive x