∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {t : Set α} {x : α}
  [(nhds x).IsCountablyGenerated],
  IsGLB t x →
    x ∉ t →
      t.Nonempty →
        ∃ u, StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t