theorem :: OPPCAT_1:11

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