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 F9 = (x1,x2) --> ((opp p1),(opp p2));
now :: thesis: for x being set st x in {x1,x2} holds
(opp ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((opp p1),(opp p2))) /. x
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 ;
hence (opp ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((opp p1),(opp p2))) /. x by ; :: thesis: verum
end;
hence opp ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((opp p1),(opp p2)) by Th1; :: thesis: verum