let R1, R2 be Relation of F₁(),F₂(); :: thesis: ( ( for x being Element of F₁()
for y being Element of F₂() holds
( [x,y] in R1 iff P₁[x,y] ) ) & ( for x being Element of F₁()
for y being Element of F₂() holds
( [x,y] in R2 iff P₁[x,y] ) ) implies R1 = R2 )
assume that
A1: for x being Element of F₁()
for y being Element of F₂() holds
( [x,y] in R1 iff P₁[x,y] ) and
A2: for x being Element of F₁()
for y being Element of F₂() holds
( [x,y] in R2 iff P₁[x,y] ) ; :: thesis: R1 = R2
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )

hereby :: thesis: ( not [x,y] in R2 or [x,y] in R1 )

assume A3: [x,y] in R1 ; :: thesis: [x,y] in R2
then reconsider a = x as Element of F₁() by ZFMISC_1:87;
reconsider b = y as Element of F₂() by A3, ZFMISC_1:87;
P₁[a,b] by A1, A3;
hence [x,y] in R2 by A2; :: thesis: verum

end;

assume A4: [x,y] in R2 ; :: thesis: [x,y] in R1
then reconsider a = x as Element of F₁() by ZFMISC_1:87;
reconsider b = y as Element of F₂() by A4, ZFMISC_1:87;
P₁[a,b] by A2, A4;
hence [x,y] in R1 by A1; :: thesis: verum