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:106;
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 ( a in {x,y} & b in {x,y} ) ; :: thesis: [a,b] in T
then ( ( a = x or a = y ) & ( b = x or b = y ) ) by TARSKI:def 2;
hence [a,b] in T by A1, A2, Th27, EQREL_1:12; :: thesis: verum

end;

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