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

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