let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for t1 being Element of T

for r being Real st 0 < r holds

diameter (Ball (t1,r)) <= 2 * r

let t1 be Element of T; :: thesis: for r being Real st 0 < r holds

diameter (Ball (t1,r)) <= 2 * r

let r be Real; :: thesis: ( 0 < r implies diameter (Ball (t1,r)) <= 2 * r )

A1: for x, y being Point of T st x in Ball (t1,r) & y in Ball (t1,r) holds

dist (x,y) <= 2 * r

then t1 in Ball (t1,r) by Th11;

hence diameter (Ball (t1,r)) <= 2 * r by A1, Def8; :: thesis: verum

for r being Real st 0 < r holds

diameter (Ball (t1,r)) <= 2 * r

let t1 be Element of T; :: thesis: for r being Real st 0 < r holds

diameter (Ball (t1,r)) <= 2 * r

let r be Real; :: thesis: ( 0 < r implies diameter (Ball (t1,r)) <= 2 * r )

A1: for x, y being Point of T st x in Ball (t1,r) & y in Ball (t1,r) holds

dist (x,y) <= 2 * r

proof

assume
0 < r
; :: thesis: diameter (Ball (t1,r)) <= 2 * r
let x, y be Point of T; :: thesis: ( x in Ball (t1,r) & y in Ball (t1,r) implies dist (x,y) <= 2 * r )

assume ( x in Ball (t1,r) & y in Ball (t1,r) ) ; :: thesis: dist (x,y) <= 2 * r

then ( dist (t1,x) < r & dist (t1,y) < r ) by METRIC_1:11;

then A2: (dist (t1,x)) + (dist (t1,y)) < r + r by XREAL_1:8;

dist (x,y) <= (dist (x,t1)) + (dist (t1,y)) by METRIC_1:4;

hence dist (x,y) <= 2 * r by A2, XXREAL_0:2; :: thesis: verum

end;assume ( x in Ball (t1,r) & y in Ball (t1,r) ) ; :: thesis: dist (x,y) <= 2 * r

then ( dist (t1,x) < r & dist (t1,y) < r ) by METRIC_1:11;

then A2: (dist (t1,x)) + (dist (t1,y)) < r + r by XREAL_1:8;

dist (x,y) <= (dist (x,t1)) + (dist (t1,y)) by METRIC_1:4;

hence dist (x,y) <= 2 * r by A2, XXREAL_0:2; :: thesis: verum

then t1 in Ball (t1,r) by Th11;

hence diameter (Ball (t1,r)) <= 2 * r by A1, Def8; :: thesis: verum