theorem :: CAT_3:12

for x1, x2 being set
for C being Category st x1 <> x2 holds
for p1, p2 being Morphism of (C opp) holds opp ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((opp p1),(opp p2))