theorem
for
C being
category for
c,
c1,
c2,
d being
Object of
C for
f1 being
Morphism of
c1,
c for
f2 being
Morphism of
c2,
c for
p1 being
Morphism of
d,
c1 for
p2 being
Morphism of
d,
c2 st
Hom (
c1,
c)
<> {} &
Hom (
c2,
c)
<> {} &
Hom (
d,
c1)
<> {} &
Hom (
d,
c2)
<> {} &
d,
p1,
p2 is_pullback_of f1,
f2 holds
d,
p2,
p1 is_pullback_of f2,
f1