let a be real number ; :: thesis: 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 ; :: thesis: ( a >= diameter ([#] M) implies dist_toler M,a = (dist_toler M,a) [*] )
assume A1: a >= diameter ([#] M) ; :: thesis: dist_toler M,a = (dist_toler M,a) [*]
A2: dist_toler M,a c= (dist_toler M,a) [*] by LANG1:18;
(dist_toler M,a) [*] c= nabla the carrier of M ;
then (dist_toler M,a) [*] c= dist_toler M,a by A1, Th37;
hence dist_toler M,a = (dist_toler M,a) [*] by A2, XBOOLE_0:def 10; :: thesis: verum