let X be set ; :: thesis: for R, T being Tolerance of X st ( for x being set st x in X holds
neighbourhood (,) c= neighbourhood (,) ) holds
R c= T
let R, T 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 be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in R or [x,b₁] in T )
let y be set ; :: 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, Th54;
hence [x,y] in T by A3, Th54; :: thesis: verum