let X be set ; :: thesis: for T being Tolerance of X
for x being set
for Y being TolClass of T st x in Y holds
Y c= neighbourhood (,)
let T be Tolerance of X; :: thesis: for x being set
for Y being TolClass of T st x in Y holds
Y c= neighbourhood (,)
let x be set ; :: thesis: for Y being TolClass of T st x in Y holds
Y c= neighbourhood (,)
let Y be TolClass of T; :: thesis: ( x in Y implies Y c= neighbourhood (,) )
assume A1: x in Y ; :: thesis: Y c= neighbourhood (,)
for y being object st y in Y holds
y in neighbourhood (,)

proof

let y be object ; :: thesis: ( y in Y implies y in neighbourhood (,) )
assume y in Y ; :: thesis: y in neighbourhood (,)
then [x,y] in T by A1, Def1;
hence y in neighbourhood (,) by Th27; :: thesis: verum

end;

hence Y c= neighbourhood (,) ; :: thesis: verum