let M be non empty Reflexive symmetric MetrStruct ; :: thesis: for a being Real

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; :: 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 that

A1: T = dist_toler (M,a) and

A2: a >= 0 ; :: thesis: T is Tolerance of the carrier of M

A3: ( the distance of M is symmetric & the distance of M is Reflexive ) by METRIC_1:def 6, METRIC_1:def 8;

T = low_toler ( the distance of M,a) by A1, Th33;

hence T is Tolerance of the carrier of M by A2, A3, Th18; :: thesis: verum

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; :: 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 that

A1: T = dist_toler (M,a) and

A2: a >= 0 ; :: thesis: T is Tolerance of the carrier of M

A3: ( the distance of M is symmetric & the distance of M is Reflexive ) by METRIC_1:def 6, METRIC_1:def 8;

T = low_toler ( the distance of M,a) by A1, Th33;

hence T is Tolerance of the carrier of M by A2, A3, Th18; :: thesis: verum