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 set st y in Y holds
y in neighbourhood ,

proof

let y be set ; :: thesis: ( y in Y implies y in neighbourhood , )
assume y in Y ; :: thesis: y in neighbourhood ,
then [x,y] in T by A1, Def3;
hence y in neighbourhood , by Th54; :: thesis: verum

end;

hence Y c= neighbourhood , by TARSKI:def 3; :: thesis: verum