let X be set ; 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; ( ( 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
; 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 ;
( 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
;
[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;
verum
end;
then
T is_transitive_in field T
;
hence
T is transitive
; verum