let R1, R2 be Relation of F1(),F2(); ( ( 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] )
; R1 = R2
let x, y be object ; RELAT_1:def 2 ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )
hereby ( not [x,y] in R2 or [x,y] in R1 )
end;
assume A4:
[x,y] in R2
; [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; verum