theorem :: CAT_1:51

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