∀ {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z},
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₁) →
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₂) →
      ∀ (i₃ : S ⟶ T) [H₃ : CategoryTheory.Mono i₃]
        (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
        (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂),
        Topology.IsOpenEmbedding
          ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))