set XX = [:X,X:];
let P, Q be Relation of [:X,X:]; :: thesis: ( ( for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) & ( for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in Q iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) implies P = Q )
assume that
A4: for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in P iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) and
A5: for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in Q iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ; :: thesis: P = Q
for x, y being set holds
( [x,y] in P iff [x,y] in Q )

proof

let x, y be set ; :: thesis: ( [x,y] in P iff [x,y] in Q )

A6: now

assume A7: [x,y] in P ; :: thesis: [x,y] in Q
then A8: ( x in [:X,X:] & y in [:X,X:] ) by ZFMISC_1:106;
then A9: ex a, b being Element of X st x = [a,b] by DOMAIN_1:9;
consider c, d being Element of X such that
A10: y = [c,d] by A8, DOMAIN_1:9;
( [x,y] in P iff ( [x,y] in R or [x,[d,c]] in R ) ) by A4, A9, A10;
hence [x,y] in Q by A5, A7, A9, A10; :: thesis: verum

end;

now

assume A11: [x,y] in Q ; :: thesis: [x,y] in P
then A12: ( x in [:X,X:] & y in [:X,X:] ) by ZFMISC_1:106;
then A13: ex a, b being Element of X st x = [a,b] by DOMAIN_1:9;
consider c, d being Element of X such that
A14: y = [c,d] by A12, DOMAIN_1:9;
( [x,y] in Q iff ( [x,y] in R or [x,[d,c]] in R ) ) by A5, A13, A14;
hence [x,y] in P by A4, A11, A13, A14; :: thesis: verum

end;

hence ( [x,y] in P iff [x,y] in Q ) by A6; :: thesis: verum

end;

hence P = Q by RELAT_1:def 2; :: thesis: verum