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

[c,d] in R2

( [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

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

[c,d] in R2

proof

hence
R1 = R2
by A4, RELAT_1:def 2; :: thesis: verum
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;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