let X be set ; :: thesis: for T, R being Tolerance of X st ( for Z being set holds
( Z is TolClass of T iff Z is TolClass of R ) ) holds
T = R
let T, R be Tolerance of X; :: thesis: ( ( for Z being set holds
( Z is TolClass of T iff Z is TolClass of R ) ) implies T = R )
assume A1: for Z being set holds
( Z is TolClass of T iff Z is TolClass of R ) ; :: 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 consider Z being TolClass of T such that
A2: ( x in Z & y in Z ) by Th20;
reconsider Z = Z as TolClass of R by A1;
Z is TolSet of R ;
hence [x,y] in R by A2, Def1; :: thesis: verum

end;

assume [x,y] in R ; :: thesis: [x,y] in T
then consider Z being TolClass of R such that
A3: ( x in Z & y in Z ) by Th20;
reconsider Z = Z as TolClass of T by A1;
Z is TolSet of T ;
hence [x,y] in T by A3, Def1; :: thesis: verum

end;

hence T = R ; :: thesis: verum