theorem Th12: :: CAT_5:12

for C being Categorial Category
for a being Object of C holds a is Category