let Y be set ; :: thesis: for T, R being Tolerance of (union Y) st ( for x, y being object holds
( [x,y] in T iff ex Z being set st
( Z in Y & x in Z & y in Z ) ) ) & ( for x, y being object holds
( [x,y] in R iff ex Z being set st
( Z in Y & x in Z & y in Z ) ) ) holds
T = R
let T, R be Tolerance of (union Y); :: thesis: ( ( for x, y being object holds
( [x,y] in T iff ex Z being set st
( Z in Y & x in Z & y in Z ) ) ) & ( for x, y being object holds
( [x,y] in R iff ex Z being set st
( Z in Y & x in Z & y in Z ) ) ) implies T = R )
assume that
A1: for x, y being object holds
( [x,y] in T iff ex Z being set st
( Z in Y & x in Z & y in Z ) ) and
A2: for x, y being object holds
( [x,y] in R iff ex Z being set st
( Z in Y & x in Z & y in Z ) ) ; :: thesis: T = R
for x, y being object holds
( [x,y] in T iff [x,y] in R )

proof

let x, y be object ; :: thesis: ( [x,y] in T iff [x,y] in R )
thus ( [x,y] in T implies [x,y] in R ) :: thesis: ( [x,y] in R implies [x,y] in T )

proof

assume [x,y] in T ; :: thesis: [x,y] in R
then ex Z being set st
( Z in Y & x in Z & y in Z ) by A1;
hence [x,y] in R by A2; :: thesis: verum

end;

assume [x,y] in R ; :: thesis: [x,y] in T
then ex Z being set st
( Z in Y & x in Z & y in Z ) by A2;
hence [x,y] in T by A1; :: thesis: verum

end;

hence T = R ; :: thesis: verum