let M be non empty Reflexive symmetric MetrStruct ; 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; 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; ( 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
; 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; verum