for C being Category
for E being Subcategory of C holds the carrier' of E c= the carrier' of C