let x1, x2 be set ; :: thesis: 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)
let C be Category; :: thesis: ( x1 <> x2 implies for p1, p2 being Morphism of (C opp ) holds opp (x1,x2 --> p1,p2) = x1,x2 --> (opp p1),(opp p2) )
assume A1: x1 <> x2 ; :: thesis: for p1, p2 being Morphism of (C opp ) holds opp (x1,x2 --> p1,p2) = x1,x2 --> (opp p1),(opp p2)
let p1, p2 be Morphism of (C opp ); :: thesis: opp (x1,x2 --> p1,p2) = x1,x2 --> (opp p1),(opp p2)
set F = x1,x2 --> p1,p2;
set F' = x1,x2 --> (opp p1),(opp p2);

now

let x be set ; :: thesis: ( x in {x1,x2} implies (opp (x1,x2 --> p1,p2)) /. x = (x1,x2 --> (opp p1),(opp p2)) /. x )
assume A2: x in {x1,x2} ; :: thesis: (opp (x1,x2 --> p1,p2)) /. x = (x1,x2 --> (opp p1),(opp p2)) /. x
then ( x = x1 or x = x2 ) by TARSKI:def 2;
then ( ( (x1,x2 --> p1,p2) /. x = p1 & (x1,x2 --> (opp p1),(opp p2)) /. x = opp p1 ) or ( (x1,x2 --> p1,p2) /. x = p2 & (x1,x2 --> (opp p1),(opp p2)) /. x = opp p2 ) ) by A1, Th7;
hence (opp (x1,x2 --> p1,p2)) /. x = (x1,x2 --> (opp p1),(opp p2)) /. x by A2, Def6; :: thesis: verum

end;

hence opp (x1,x2 --> p1,p2) = x1,x2 --> (opp p1),(opp p2) by Th1; :: thesis: verum