theorem Th27: :: YELLOW20:27

for A being category
for C being non empty subcategory of A
for a, b being Object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds (incl C) . f = f