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
for c, d being set holds
( [c,d] in A iff [c,d] in B )

proof

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

proof

let c, d be set ; :: thesis: ( [c,d] in A implies [c,d] in B )
assume A5: [c,d] in A ; :: thesis: [c,d] in B
then reconsider c1 = c, d1 = d as Element of M by ZFMISC_1:106;
c1,d1 are_in_tolerance_wrt a by A2, A5;
hence [c,d] in B by A3; :: thesis: verum

end;

for c, d being set st [c,d] in B holds
[c,d] in A

proof

let c, d be set ; :: thesis: ( [c,d] in B implies [c,d] in A )
assume A6: [c,d] in B ; :: thesis: [c,d] in A
then reconsider c1 = c, d1 = d as Element of M by ZFMISC_1:106;
c1,d1 are_in_tolerance_wrt a by A3, A6;
hence [c,d] in A by A2; :: thesis: verum

end;

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

end;

hence A = B by RELAT_1:def 2; :: thesis: verum