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:106;
then A3: neighbourhood , c= neighbourhood , by A1;
y in neighbourhood , by A2, Th54;
hence [x,y] in T by A3, Th54; :: thesis: verum