theorem :: ALTCAT_4:11

for C being category
for o1, o2 being Object of C st o1 is initial & o1,o2 are_iso holds
o2 is initial