theorem :: CAT_3:9

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