let a, b be set ; :: thesis: ( ( for x being set holds
( x in a iff x is Tolerance of X ) ) & ( for x being set holds
( x in b iff x is Tolerance of X ) ) implies a = b )
assume that
A2: for x being set holds
( x in a iff x is Tolerance of X ) and
A3: for x being set holds
( x in b iff x is Tolerance of X ) ; :: thesis: a = b

now :: thesis: for x being set holds
( x in a iff x in b )

let x be set ; :: thesis: ( x in a iff x in b )

A4: now :: thesis: ( x in b implies x in a )

assume x in b ; :: thesis: x in a
then x is Tolerance of X by A3;
hence x in a by A2; :: thesis: verum

end;

now :: thesis: ( x in a implies x in b )

assume x in a ; :: thesis: x in b
then x is Tolerance of X by A2;
hence x in b by A3; :: thesis: verum

end;

hence ( x in a iff x in b ) by A4; :: thesis: verum

end;

hence a = b by TARSKI:1; :: thesis: verum