let X be set ; :: thesis: for T being Tolerance of X holds rng T = X
let T be Tolerance of X; :: thesis: rng T = X
for x being object holds
( x in rng T iff x in X )

proof

let x be object ; :: thesis: ( x in rng T iff x in X )
( x in X implies x in rng T )

proof

field T = X by ORDERS_1:12;
then A1: T is_reflexive_in X by RELAT_2:def 9;
assume x in X ; :: thesis: x in rng T
then [x,x] in T by A1;
hence x in rng T by XTUPLE_0:def 13; :: thesis: verum

end;

hence ( x in rng T iff x in X ) ; :: thesis: verum

end;

hence rng T = X by TARSKI:2; :: thesis: verum