theorem :: GRCAT_1:5

for C being Category
for O being non empty Subset of the carrier of C holds the carrier of (cat O) = O ;