∀ (Z : TopCat) (f : Z ⟶ { carrier := PUnit.{u_1 + 1} ⊕ PUnit.{u_1 + 1}, str := instTopologicalSpaceSum }),
  Set.range
        ⇑(CategoryTheory.ConcreteCategory.hom
            (TopCat.pullbackFst f
              ({ carrier := PUnit.{u_1 + 1}, str := instTopologicalSpacePUnit }.binaryCofan
                  { carrier := PUnit.{u_1 + 1}, str := instTopologicalSpacePUnit }).inl)) =
      ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl →
    Set.range
          ⇑(CategoryTheory.ConcreteCategory.hom
              (TopCat.pullbackFst f
                ({ carrier := PUnit.{u_1 + 1}, str := instTopologicalSpacePUnit }.binaryCofan
                    { carrier := PUnit.{u_1 + 1}, str := instTopologicalSpacePUnit }).inr)) =
        ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr →
      Nonempty
        (CategoryTheory.Limits.IsColimit
          (CategoryTheory.Limits.BinaryCofan.mk
            (TopCat.pullbackFst f
              ({ carrier := PUnit.{u_1 + 1}, str := instTopologicalSpacePUnit }.binaryCofan
                  { carrier := PUnit.{u_1 + 1}, str := instTopologicalSpacePUnit }).inl)
            (TopCat.pullbackFst f
              ({ carrier := PUnit.{u_1 + 1}, str := instTopologicalSpacePUnit }.binaryCofan
                  { carrier := PUnit.{u_1 + 1}, str := instTopologicalSpacePUnit }).inr)))