theorem Th10: :: CAT_2:14

for C being Category
for E being Subcategory of C
for a being Object of E holds (Obj (incl E)) . a = a