let A, B be Relation of M; :: thesis: ( ( for x, y being Element of M holds

( [x,y] in A iff x,y are_in_tolerance_wrt a ) ) & ( for x, y being Element of M holds

( [x,y] in B iff x,y are_in_tolerance_wrt a ) ) implies A = B )

assume that

A2: for x, y being Element of M holds

( [x,y] in A iff x,y are_in_tolerance_wrt a ) and

A3: for x, y being Element of M holds

( [x,y] in B iff x,y are_in_tolerance_wrt a ) ; :: thesis: A = B

A4: for c, d being object st [c,d] in B holds

[c,d] in A

[c,d] in B

( [x,y] in A iff x,y are_in_tolerance_wrt a ) ) & ( for x, y being Element of M holds

( [x,y] in B iff x,y are_in_tolerance_wrt a ) ) implies A = B )

assume that

A2: for x, y being Element of M holds

( [x,y] in A iff x,y are_in_tolerance_wrt a ) and

A3: for x, y being Element of M holds

( [x,y] in B iff x,y are_in_tolerance_wrt a ) ; :: thesis: A = B

A4: for c, d being object st [c,d] in B holds

[c,d] in A

proof

for c, d being object st [c,d] in A holds
let c, d be object ; :: thesis: ( [c,d] in B implies [c,d] in A )

assume A5: [c,d] in B ; :: thesis: [c,d] in A

then reconsider c1 = c, d1 = d as Element of M by ZFMISC_1:87;

c1,d1 are_in_tolerance_wrt a by A3, A5;

hence [c,d] in A by A2; :: thesis: verum

end;assume A5: [c,d] in B ; :: thesis: [c,d] in A

then reconsider c1 = c, d1 = d as Element of M by ZFMISC_1:87;

c1,d1 are_in_tolerance_wrt a by A3, A5;

hence [c,d] in A by A2; :: thesis: verum

[c,d] in B

proof

hence
A = B
by A4, RELAT_1:def 2; :: thesis: verum
let c, d be object ; :: thesis: ( [c,d] in A implies [c,d] in B )

assume A6: [c,d] in A ; :: thesis: [c,d] in B

then reconsider c1 = c, d1 = d as Element of M by ZFMISC_1:87;

c1,d1 are_in_tolerance_wrt a by A2, A6;

hence [c,d] in B by A3; :: thesis: verum

end;assume A6: [c,d] in A ; :: thesis: [c,d] in B

then reconsider c1 = c, d1 = d as Element of M by ZFMISC_1:87;

c1,d1 are_in_tolerance_wrt a by A2, A6;

hence [c,d] in B by A3; :: thesis: verum