theorem Th1: :: CAT_7:1

for C being CategoryStr
for f being morphism of C st not C is empty holds
f in the carrier of C