theorem Th10: :: ALTCAT_2:10
for C being Category
for i, j, k being Object of C holds [:(Hom (j,k)),(Hom (i,j)):] c= dom the Comp of C