theorem Th10: :: CAT_5:10

for C, D being Category st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) & C is Categorial holds
D is Categorial