theorem :: CAT_1:55

for C being Category
for a, b being Object of C st a is terminal & b is terminal holds
a,b are_isomorphic