theorem :: CAT_3:11

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