theorem Th3: :: CAT_2:7

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