let X be set ; :: thesis: for T being Tolerance of X
for x, y being set st [x,y] in T holds
ex Z being TolClass of T st
( x in Z & y in Z )
let T be Tolerance of X; :: thesis: for x, y being set st [x,y] in T holds
ex Z being TolClass of T st
( x in Z & y in Z )
let x, y be set ; :: thesis: ( [x,y] in T implies ex Z being TolClass of T st
( x in Z & y in Z ) )
assume A1: [x,y] in T ; :: thesis: ex Z being TolClass of T st
( x in Z & y in Z )
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;

then reconsider PS = {x,y} as TolSet of T by Def3;
consider Z being TolClass of T such that
A3: PS c= Z by Th45;
take Z ; :: thesis: ( x in Z & y in Z )
x in {x,y} by TARSKI:def 2;
hence x in Z by A3; :: thesis: y in Z
y in {x,y} by TARSKI:def 2;
hence y in Z by A3; :: thesis: verum