theorem :: CAT_2:15

for C being Category
for E being Subcategory of C
for a being Object of E holds (incl E) . a = a by Th10;