theorem Th6: :: NATTRA_1:10

for C being strict Category
for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds
A = C