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:12;
then A3: T is_transitive_in X by A1;
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, Th27;
then A6: [y,x] in T by EQREL_1:6;
[x,z] in T by A5, Th27;
hence [y,z] in T by A3, A2, A4, A5, A6; :: thesis: verum
end;
then reconsider Z = Class (T,x) as TolSet of T by Def1;
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:20;
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:6;
hence contradiction by A7, Th27; :: thesis: verum
end;
hence neighbourhood (,) is TolClass of T by Def2; :: thesis: verum