let X, x be set ; :: thesis:
let T be Tolerance of X; :: thesis:
let Y be set ; :: thesis:
assume A1: for Z being set holds
( Z in Y iff ( x in Z & Z is TolSet of T ) ) ; :: thesis:
for y being object holds
( y in neighbourhood (,) iff y in union Y )

assume y in neighbourhood (,) ; :: thesis:
then [x,y] in T by Th27;
then consider Z being TolClass of T such that
A2: x in Z and
A3: y in Z by Th20;
Z in Y by A1, A2;
hence y in union Y by A3, TARSKI:def 4; :: thesis:

end;

assume y in union Y ; :: thesis:
then consider Z being set such that
A4: y in Z and
A5: Z in Y by TARSKI:def 4;
reconsider Z = Z as TolSet of T by A1, A5;
x in Z by A1, A5;
then [x,y] in T by A4, Def1;
hence y in neighbourhood (,) by Th27; :: thesis:

end;