∀ {X : Type u_1} [inst : TopologicalSpace X],
  (∀ (F : Set X),
      IsClosed F →
        ∃ fseq,
          (∀ (n : ℕ) (x : X), (fseq n) x ≤ 1) ∧
            (∀ (n : ℕ), ∀ x ∈ F, 1 ≤ (fseq n) x) ∧
              Filter.Tendsto (fun n x => (fseq n) x) Filter.atTop (nhds (F.indicator fun x => 1))) →
    HasOuterApproxClosed X