for C, D being category st C is terminal & C ~= D holds
D is terminal