let R1, R2 be Relation of F1(),F2(); :: thesis: ( ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R1 iff P1[x,y] ) ) & ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R2 iff P1[x,y] ) ) implies R1 = R2 )
assume that
A1: for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R1 iff P1[x,y] ) and
A2: for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R2 iff P1[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 F1() by ZFMISC_1:87;
reconsider b = y as Element of F2() by A3, ZFMISC_1:87;
P1[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 F1() by ZFMISC_1:87;
reconsider b = y as Element of F2() by A4, ZFMISC_1:87;
P1[a,b] by A2, A4;
hence [x,y] in R1 by A1; :: thesis: verum