let X be set ; :: thesis: for T being Tolerance of X
for x, y being set st [x,y] in T holds
{x,y} is TolSet of T
let T be Tolerance of X; :: thesis: for x, y being set st [x,y] in T holds
{x,y} is TolSet of T
let x, y be set ; :: thesis: ( [x,y] in T implies {x,y} is TolSet of T )
assume A1: [x,y] in T ; :: thesis: {x,y} is TolSet of T
then A2: ( x in X & y in X ) by ZFMISC_1:87;
for a, b being set st a in {x,y} & b in {x,y} holds
[a,b] in T

proof

let a, b be set ; :: thesis: ( a in {x,y} & b in {x,y} implies [a,b] in T )
assume that
A3: a in {x,y} and
A4: b in {x,y} ; :: thesis: [a,b] in T
A5: ( b = x or b = y ) by A4, TARSKI:def 2;
( a = x or a = y ) by A3, TARSKI:def 2;
hence [a,b] in T by A1, A2, A5, Th7, EQREL_1:6; :: thesis: verum

end;

hence {x,y} is TolSet of T by Def1; :: thesis: verum