let R1, R2 be Relation of X; :: thesis: ( ( for x, y being Element of X holds
( [x,y] in R1 iff f . x,y <= a ) ) & ( for x, y being Element of X holds
( [x,y] in R2 iff f . x,y <= a ) ) implies R1 = R2 )
assume that
A2: for x, y being Element of X holds
( [x,y] in R1 iff f . x,y <= a ) and
A3: for x, y being Element of X holds
( [x,y] in R2 iff f . x,y <= a ) ; :: thesis: R1 = R2
for c, d being set holds
( [c,d] in R1 iff [c,d] in R2 )

proof

A4: for c, d being set st [c,d] in R1 holds
[c,d] in R2

proof

let c, d be set ; :: thesis: ( [c,d] in R1 implies [c,d] in R2 )
assume A5: [c,d] in R1 ; :: thesis: [c,d] in R2
then reconsider c1 = c, d1 = d as Element of X by ZFMISC_1:106;
f . c1,d1 <= a by A2, A5;
hence [c,d] in R2 by A3; :: thesis: verum

end;

for c, d being set st [c,d] in R2 holds
[c,d] in R1

proof

let c, d be set ; :: thesis: ( [c,d] in R2 implies [c,d] in R1 )
assume A6: [c,d] in R2 ; :: thesis: [c,d] in R1
then reconsider c1 = c, d1 = d as Element of X by ZFMISC_1:106;
f . c1,d1 <= a by A3, A6;
hence [c,d] in R1 by A2; :: thesis: verum

end;

hence for c, d being set holds
( [c,d] in R1 iff [c,d] in R2 ) by A4; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum