let X be set ; :: thesis: for T being Tolerance of X st ( for x being set st x in X holds
neighbourhood (,) is TolSet of T ) holds
T is transitive
let T be Tolerance of X; :: thesis: ( ( for x being set st x in X holds
neighbourhood (,) is TolSet of T ) implies T is transitive )
assume A1: for x being set st x in X holds
neighbourhood (,) is TolSet of T ; :: thesis: T is transitive
A2: field T = X by ORDERS_1:12;
for x, y, z being object st x in field T & y in field T & z in field T & [x,y] in T & [y,z] in T holds
[x,z] in T

proof

let x, y, z be object ; :: thesis: ( x in field T & y in field T & z in field T & [x,y] in T & [y,z] in T implies [x,z] in T )
assume that
x in field T and
A3: y in field T and
z in field T and
A4: [x,y] in T and
A5: [y,z] in T ; :: thesis: [x,z] in T
reconsider N = neighbourhood (,) as TolSet of T by A2, A1, A3;
[y,x] in T by A4, EQREL_1:6;
then A6: x in N by Th27;
z in N by A5, Th27;
hence [x,z] in T by A6, Def1; :: thesis: verum

end;

then T is_transitive_in field T ;
hence T is transitive ; :: thesis: verum