let a be real number ; :: 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

now

let z be set ; :: thesis: ( z in nabla the carrier of M implies z in dist_toler M,a )
assume A2: z in nabla the carrier of M ; :: thesis: z in dist_toler M,a
consider x, y being set such that
A3: ( x in the carrier of M & y in the carrier of M ) and
A4: z = [x,y] by A2, ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Element of M by A3;
dist x1,y1 <= diameter ([#] M) by TBSP_1:def 10;
then dist x1,y1 <= a by A1, XXREAL_0:2;
then x1,y1 are_in_tolerance_wrt a by Def6;
hence z in dist_toler M,a by A4, Def7; :: thesis: verum

end;

then nabla the carrier of M c= dist_toler M,a by TARSKI:def 3;
hence dist_toler M,a = nabla the carrier of M by XBOOLE_0:def 10; :: thesis: verum