let X be set ; :: thesis: for T, R being Tolerance of X st ( for x being set st x in X holds
neighbourhood (,) c= neighbourhood (,) ) holds
R c= T
let T, R be Tolerance of X; :: thesis: ( ( for x being set st x in X holds
neighbourhood (,) c= neighbourhood (,) ) implies R c= T )
assume A1: for x being set st x in X holds
neighbourhood (,) c= neighbourhood (,) ; :: thesis: R c= T
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R or [x,y] in T )
assume A2: [x,y] in R ; :: thesis: [x,y] in T
then x in X by ZFMISC_1:87;
then A3: neighbourhood (,) c= neighbourhood (,) by A1;
y in neighbourhood (,) by A2, Th27;
hence [x,y] in T by A3, Th27; :: thesis: verum