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:19;
hence [x,y] in T by EQREL_1:6; :: thesis: verum

end;

assume [x,y] in T ; :: thesis: y in neighbourhood (,)
then [y,x] in T by EQREL_1:6;
hence y in neighbourhood (,) by EQREL_1:19; :: thesis: verum