theorem Th25: :: CAT_8:25

for C, D being terminal category holds C ~= D