let M be non empty Reflexive symmetric MetrStruct ; :: thesis: for a being real number
for T being Relation of the carrier of M,the carrier of M st T = dist_toler M,a & a >= 0 holds
T is Tolerance of the carrier of M
let a be real number ; :: thesis: for T being Relation of the carrier of M,the carrier of M st T = dist_toler M,a & a >= 0 holds
T is Tolerance of the carrier of M
let T be Relation of the carrier of M,the carrier of M; :: thesis: ( T = dist_toler M,a & a >= 0 implies T is Tolerance of the carrier of M )
assume A1: ( T = dist_toler M,a & a >= 0 ) ; :: thesis: T is Tolerance of the carrier of M
A2: the distance of M is symmetric by METRIC_1:def 9;
A3: the distance of M is Reflexive by METRIC_1:def 7;
T = low_toler the distance of M,a by A1, Th33;
hence T is Tolerance of the carrier of M by A1, A2, A3, Th18; :: thesis: verum