theorem :: OPPCAT_1:66

for C being Category
for c being Object of C holds (Obj (id* C)) . c = c opp