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
A5: 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
A6: 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 object holds
( [x,y] in P iff [x,y] in Q )

proof

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

A7: now :: thesis: ( [x,y] in Q implies [x,y] in P )

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

end;

now :: thesis: ( [x,y] in P implies [x,y] in Q )

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

end;

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

end;

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