let a be Real; for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
dist_toler (M,a) = (dist_toler (M,a)) [*]
let M be non empty Reflexive symmetric bounded MetrStruct ; ( a >= diameter ([#] M) implies dist_toler (M,a) = (dist_toler (M,a)) [*] )
assume A1:
a >= diameter ([#] M)
; dist_toler (M,a) = (dist_toler (M,a)) [*]
(dist_toler (M,a)) [*] c= nabla the carrier of M
;
then
( dist_toler (M,a) c= (dist_toler (M,a)) [*] & (dist_toler (M,a)) [*] c= dist_toler (M,a) )
by A1, Th37, LANG1:18;
hence
dist_toler (M,a) = (dist_toler (M,a)) [*]
by XBOOLE_0:def 10; verum