set XX = [:X,X:];
let P, Q be Relation of [:X,X:]; ( ( 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 ) )
; P = Q
for x, y being object holds
( [x,y] in P iff [x,y] in Q )
proof
let x,
y be
object ;
( [x,y] in P iff [x,y] in Q )
A7:
now ( [x,y] in Q implies [x,y] in P )assume A8:
[x,y] in Q
;
[x,y] in Pthen
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;
verum end;
now ( [x,y] in P implies [x,y] in Q )assume A11:
[x,y] in P
;
[x,y] in Qthen
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;
verum end;
hence
(
[x,y] in P iff
[x,y] in Q )
by A7;
verum
end;
hence
P = Q
by RELAT_1:def 2; verum