theorem Th10: :: YELLOW18:10

for A, B being category st A,B are_opposite holds
for a being Object of A
for b being Object of B st a = b holds
idm a = idm b