for a being Real
for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
(dist_toler (M,a)) [*] = nabla the carrier of M