theorem Th2: :: CAT_7:2

for C being with_identities CategoryStr
for a being Object of C st not C is empty holds
a in the carrier of C