for C being category
for c1, c2, c3, c4, c5, c6 being Object of C
for f1 being Morphism of c1,c2
for f2 being Morphism of c2,c3
for f3 being Morphism of c1,c4
for f4 being Morphism of c2,c5
for f5 being Morphism of c3,c6
for f6 being Morphism of c4,c5
for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds
( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )