theorem Th4: :: CAT_2:8

for C being Category
for E being Subcategory of C
for f being Morphism of E holds f is Morphism of C