theorem :: CAT_8:21

for C being composable with_identities CategoryStr
for a, b being Object of C st a is terminal & b is terminal holds
a,b are_isomorphic