theorem :: ALTCAT_3:29

for C being category
for o1, o2 being Object of C st o1 is _zero & o2 is _zero holds
o1,o2 are_iso by Th26;