theorem Th65: :: CAT_3:65

for x1, x2 being set
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds
(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}