∀ {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) =
    {x | ∃ y, (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) y}