let X be set ; :: thesis: for T being Tolerance of X st T is transitive holds
for x being set st x in X holds
neighbourhood , is TolClass of T
let T be Tolerance of X; :: thesis: ( T is transitive implies for x being set st x in X holds
neighbourhood , is TolClass of T )
assume A1: T is transitive ; :: thesis: for x being set st x in X holds
neighbourhood , is TolClass of T
let x be set ; :: thesis: ( x in X implies neighbourhood , is TolClass of T )
assume A2: x in X ; :: thesis: neighbourhood , is TolClass of T
set N = Class T,x;
field T = X by ORDERS_1:97;
then A3: T is_transitive_in X by A1, RELAT_2:def 16;
for y, z being set st y in Class T,x & z in Class T,x holds
[y,z] in T

proof

let y, z be set ; :: thesis: ( y in Class T,x & z in Class T,x implies [y,z] in T )
assume that
A4: y in Class T,x and
A5: z in Class T,x ; :: thesis: [y,z] in T
[x,y] in T by A4, Th54;
then A6: [y,x] in T by EQREL_1:12;
[x,z] in T by A5, Th54;
hence [y,z] in T by A3, A2, A4, A5, A6, RELAT_2:def 8; :: thesis: verum

end;

then reconsider Z = Class T,x as TolSet of T by Def3;
for x being set st not x in Z & x in X holds
ex y being set st
( y in Z & not [x,y] in T )

proof

let y be set ; :: thesis: ( not y in Z & y in X implies ex y being set st
( y in Z & not [y,y] in T ) )
assume that
A7: not y in Z and
y in X ; :: thesis: ex y being set st
( y in Z & not [y,y] in T )
A8: x in Z by A2, EQREL_1:28;
assume for z being set st z in Z holds
[y,z] in T ; :: thesis: contradiction
then [y,x] in T by A8;
then [x,y] in T by EQREL_1:12;
hence contradiction by A7, Th54; :: thesis: verum

end;

hence neighbourhood , is TolClass of T by Def4; :: thesis: verum