theorem Th13: :: CAT_7:13

for C, D being empty with_identities CategoryStr holds C ~= D