∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (S : CategoryTheory.Limits.PullbackCone f g),
  CategoryTheory.CategoryStruct.comp
        (TopCat.ofHom
          {
            toFun := fun x =>
              ⟨((CategoryTheory.ConcreteCategory.hom S.fst) x, (CategoryTheory.ConcreteCategory.hom S.snd) x), ⋯⟩,
            continuous_toFun := ⋯ })
        (TopCat.pullbackCone f g).fst =
      S.fst ∧
    CategoryTheory.CategoryStruct.comp
          (TopCat.ofHom
            {
              toFun := fun x =>
                ⟨((CategoryTheory.ConcreteCategory.hom S.fst) x, (CategoryTheory.ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ })
          (TopCat.pullbackCone f g).snd =
        S.snd ∧
      ∀ {m : S.pt ⟶ (TopCat.pullbackCone f g).pt},
        CategoryTheory.CategoryStruct.comp m (TopCat.pullbackCone f g).fst = S.fst →
          CategoryTheory.CategoryStruct.comp m (TopCat.pullbackCone f g).snd = S.snd →
            m =
              TopCat.ofHom
                {
                  toFun := fun x =>
                    ⟨((CategoryTheory.ConcreteCategory.hom S.fst) x, (CategoryTheory.ConcreteCategory.hom S.snd) x), ⋯⟩,
                  continuous_toFun := ⋯ }