{X : Type u_2} →
  [inst : TopologicalSpace X] →
    {P : Set X → Set X → Prop} →
      (C U : Set X) →
        P C U →
          IsClosed C →
            IsOpen U →
              C ⊆ U →
                (∀ {c u : Set X},
                    IsClosed c →
                      P c u → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P c v ∧ P (closure v) u) →
                  Urysohns.CU P