{α : Type u_1} →
  (MeasurableSet' : Set α → Prop) →
    (measurableSet_empty : MeasurableSet' ∅) →
      (measurableSet_compl : ∀ (s : Set α), MeasurableSet' s → MeasurableSet' sᶜ) →
        (measurableSet_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet' (f i)) → MeasurableSet' (⋃ i, f i)) →
          (IsOpen : Set α → Prop) →
            (isOpen_univ : IsOpen Set.univ) →
              (isOpen_inter : ∀ (s t : Set α), IsOpen s → IsOpen t → IsOpen (s ∩ t)) →
                (isOpen_sUnion : ∀ (s : Set (Set α)), (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)) →
                  { MeasurableSet' := MeasurableSet', measurableSet_empty := measurableSet_empty,
                        measurableSet_compl := measurableSet_compl, measurableSet_iUnion := measurableSet_iUnion } =
                      borel α →
                    (∃ b,
                        b.Countable ∧
                          { IsOpen := IsOpen, isOpen_univ := isOpen_univ, isOpen_inter := isOpen_inter,
                              isOpen_sUnion := isOpen_sUnion } =
                            TopologicalSpace.generateFrom b) →
                      (∃ m,
                          PseudoMetricSpace.toUniformSpace.toTopologicalSpace =
                              { IsOpen := IsOpen, isOpen_univ := isOpen_univ, isOpen_inter := isOpen_inter,
                                isOpen_sUnion := isOpen_sUnion } ∧
                            CompleteSpace α) →
                        UpgradedStandardBorel α