let r be Real; :: thesis: for M being non empty Reflexive symmetric triangle MetrStruct
for p being Point of M st 0 <= r holds
diameter (cl_Ball p,r) <= 2 * r
let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for p being Point of M st 0 <= r holds
diameter (cl_Ball p,r) <= 2 * r
let p be Point of M; :: thesis: ( 0 <= r implies diameter (cl_Ball p,r) <= 2 * r )
assume A1: 0 <= r ; :: thesis: diameter (cl_Ball p,r) <= 2 * r
A2: cl_Ball p,r is bounded by TOPREAL6:67;
dist p,p = 0 by METRIC_1:1;
then A3: p in cl_Ball p,r by A1, METRIC_1:13;

now

let x, y be Point of M; :: thesis: ( x in cl_Ball p,r & y in cl_Ball p,r implies dist x,y <= 2 * r )
assume A4: ( x in cl_Ball p,r & y in cl_Ball p,r ) ; :: thesis: dist x,y <= 2 * r
( dist p,y <= r & dist x,p <= r ) by A4, METRIC_1:13;
then ( dist x,y <= (dist x,p) + (dist p,y) & (dist x,p) + (dist p,y) <= r + r ) by METRIC_1:4, XREAL_1:9;
hence dist x,y <= 2 * r by XXREAL_0:2; :: thesis: verum

end;

hence diameter (cl_Ball p,r) <= 2 * r by A2, A3, TBSP_1:def 10; :: thesis: verum