let Y be set ; :: thesis: ex T being Tolerance of (union Y) st
for Z being set st Z in Y holds
Z is TolSet of T
defpred S₁[ set , set ] means ex Z being set st
( Z in Y & $1 in Z & $2 in Z );
A1: for x being set st x in union Y holds
S₁[x,x]

proof

let x be set ; :: thesis: ( x in union Y implies S₁[x,x] )
assume x in union Y ; :: thesis: S₁[x,x]
then ex Z being set st
( x in Z & Z in Y ) by TARSKI:def 4;
hence S₁[x,x] ; :: thesis: verum

end;

A2: for x, y being set st x in union Y & y in union Y & S₁[x,y] holds
S₁[y,x] ;
consider T being Tolerance of (union Y) such that
A3: for x, y being set st x in union Y & y in union Y holds
( [x,y] in T iff S₁[x,y] ) from TOLER_1:sch 1(A1, A2);
take T ; :: thesis: for Z being set st Z in Y holds
Z is TolSet of T
let Z be set ; :: thesis: ( Z in Y implies Z is TolSet of T )
assume A4: Z in Y ; :: thesis: Z is TolSet of T
for x, y being set st x in Z & y in Z holds
[x,y] in T

proof

let x, y be set ; :: thesis: ( x in Z & y in Z implies [x,y] in T )
assume A5: ( x in Z & y in Z ) ; :: thesis: [x,y] in T
then ( x in union Y & y in union Y ) by A4, TARSKI:def 4;
hence [x,y] in T by A3, A4, A5; :: thesis: verum

end;

hence Z is TolSet of T by Def1; :: thesis: verum