let a be Real; 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 ; ( a >= diameter ([#] M) implies dist_toler (M,a) = nabla the carrier of M )
assume A1:
a >= diameter ([#] M)
; dist_toler (M,a) = nabla the carrier of M
now for z being object st z in nabla the carrier of M holds
z in dist_toler (M,a)let z be
object ;
( z in nabla the carrier of M implies z in dist_toler (M,a) )assume
z in nabla the
carrier of
M
;
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;
verum end;
then
nabla the carrier of M c= dist_toler (M,a)
;
hence
dist_toler (M,a) = nabla the carrier of M
by XBOOLE_0:def 10; verum