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