theorem :: CAT_8:37

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