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