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:12;
A3: now :: thesis: for x, y being Point of M st x in cl_Ball (p,r) & y in cl_Ball (p,r) holds
dist (x,y) <= 2 * r
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:12;
A7: dist (x,y) <= (dist (x,p)) + (dist (p,y)) by METRIC_1:4;
dist (p,y) <= r by A5, METRIC_1:12;
then (dist (x,p)) + (dist (p,y)) <= r + r by A6, XREAL_1:7;
hence dist (x,y) <= 2 * r by A7, XXREAL_0:2; :: thesis: verum
end;
cl_Ball (p,r) is bounded by TOPREAL6:59;
hence diameter (cl_Ball (p,r)) <= 2 * r by A2, A3, TBSP_1:def 8; :: thesis: verum