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
A4: for c, d being object st [c,d] in R2 holds
[c,d] in R1

proof

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

end;

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

proof

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

end;

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