let X, x be set ; :: thesis: for T being Tolerance of X
for y being set holds
( y in neighbourhood , iff [x,y] in T )
let T be Tolerance of X; :: thesis: for y being set holds
( y in neighbourhood , iff [x,y] in T )
let y be set ; :: thesis: ( y in neighbourhood , iff [x,y] in T )

hereby :: thesis: ( [x,y] in T implies y in neighbourhood , )

assume y in neighbourhood , ; :: thesis: [x,y] in T
then [y,x] in T by EQREL_1:27;
hence [x,y] in T by EQREL_1:12; :: thesis: verum

end;

assume [x,y] in T ; :: thesis: y in neighbourhood ,
then [y,x] in T by EQREL_1:12;
hence y in neighbourhood , by EQREL_1:27; :: thesis: verum