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 )
A1: dist p,p = 0 by METRIC_1:1;
assume 0 <= r ; :: thesis: diameter (cl_Ball p,r) <= 2 * r
then A2: p in cl_Ball p,r by A1, METRIC_1:13;

A3: 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 that
A4: x in cl_Ball p,r and
A5: y in cl_Ball p,r ; :: thesis: dist x,y <= 2 * r
A6: dist x,p <= r by A4, METRIC_1:13;
A7: dist x,y <= (dist x,p) + (dist p,y) by METRIC_1:4;
dist p,y <= r by A5, METRIC_1:13;
then (dist x,p) + (dist p,y) <= r + r by A6, XREAL_1:9;
hence dist x,y <= 2 * r by A7, XXREAL_0:2; :: thesis: verum

end;

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