let a be Real; :: thesis: for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds

dist_toler (M,a) = nabla the carrier of M

let M be non empty Reflexive symmetric bounded MetrStruct ; :: thesis: ( a >= diameter ([#] M) implies dist_toler (M,a) = nabla the carrier of M )

assume A1: a >= diameter ([#] M) ; :: thesis: dist_toler (M,a) = nabla the carrier of M

hence dist_toler (M,a) = nabla the carrier of M by XBOOLE_0:def 10; :: thesis: verum

dist_toler (M,a) = nabla the carrier of M

let M be non empty Reflexive symmetric bounded MetrStruct ; :: thesis: ( a >= diameter ([#] M) implies dist_toler (M,a) = nabla the carrier of M )

assume A1: a >= diameter ([#] M) ; :: thesis: dist_toler (M,a) = nabla the carrier of M

now :: thesis: for z being object st z in nabla the carrier of M holds

z in dist_toler (M,a)

then
nabla the carrier of M c= dist_toler (M,a)
;z in dist_toler (M,a)

let z be object ; :: thesis: ( z in nabla the carrier of M implies z in dist_toler (M,a) )

assume z in nabla the carrier of M ; :: thesis: z in dist_toler (M,a)

then consider x, y being object such that

A2: ( x in the carrier of M & y in the carrier of M ) and

A3: z = [x,y] by ZFMISC_1:def 2;

reconsider x1 = x, y1 = y as Element of M by A2;

dist (x1,y1) <= diameter ([#] M) by TBSP_1:def 8;

then dist (x1,y1) <= a by A1, XXREAL_0:2;

then x1,y1 are_in_tolerance_wrt a ;

hence z in dist_toler (M,a) by A3, Def7; :: thesis: verum

end;assume z in nabla the carrier of M ; :: thesis: z in dist_toler (M,a)

then consider x, y being object such that

A2: ( x in the carrier of M & y in the carrier of M ) and

A3: z = [x,y] by ZFMISC_1:def 2;

reconsider x1 = x, y1 = y as Element of M by A2;

dist (x1,y1) <= diameter ([#] M) by TBSP_1:def 8;

then dist (x1,y1) <= a by A1, XXREAL_0:2;

then x1,y1 are_in_tolerance_wrt a ;

hence z in dist_toler (M,a) by A3, Def7; :: thesis: verum

hence dist_toler (M,a) = nabla the carrier of M by XBOOLE_0:def 10; :: thesis: verum