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