theorem :: OPPCAT_1:9

for C being Category
for a, b being Object of (C opp)
for f being Morphism of a,b holds (opp f) opp = f ;