theorem Th46: :: CAT_6:45

for C being non empty category
for o1 being Object of C
for o2 being Object of (Alter C) st o1 = o2 holds
id- o1 = id o2