theorem :: CAT_3:8

for I being set
for C being Category
for f being Morphism of C holds (I --> f) opp = I --> (f opp)