let Y be set ; 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); ( ( 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 ) )
; T = R
for x, y being object holds
( [x,y] in T iff [x,y] in R )
proof
let x,
y be
object ;
( [x,y] in T iff [x,y] in R )
thus
(
[x,y] in T implies
[x,y] in R )
( [x,y] in R implies [x,y] in T )
assume
[x,y] in R
;
[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;
verum
end;
hence
T = R
; verum