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

proof

let y be set ; :: thesis: ( y in neighbourhood , iff y in union Y )
thus ( y in neighbourhood , implies y in union Y ) :: thesis: ( y in union Y implies y in neighbourhood , )

proof

assume y in neighbourhood , ; :: thesis: y in union Y
then [x,y] in T by Th54;
then consider Z being TolClass of T such that
A2: ( x in Z & y in Z ) by Th46;
Z in Y by A1, A2;
hence y in union Y by A2, TARSKI:def 4; :: thesis: verum

end;

assume y in union Y ; :: thesis: y in neighbourhood ,
then consider Z being set such that
A3: ( y in Z & Z in Y ) by TARSKI:def 4;
reconsider Z = Z as TolClass of T by A1, A3;
x in Z by A1, A3;
then [x,y] in T by A3, Def3;
hence y in neighbourhood , by Th54; :: thesis: verum

end;

hence neighbourhood , = union Y by TARSKI:2; :: thesis: verum