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

dist_toler (M,a) = (dist_toler (M,a)) [*] by A1, Th38;

hence (dist_toler (M,a)) [*] = nabla the carrier of M by A1, Th37; :: 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

dist_toler (M,a) = (dist_toler (M,a)) [*] by A1, Th38;

hence (dist_toler (M,a)) [*] = nabla the carrier of M by A1, Th37; :: thesis: verum