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

proof

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 0 < r ; :: thesis: diameter (Ball (t1,r)) <= 2 * r
then t1 in Ball (t1,r) by Th11;
hence diameter (Ball (t1,r)) <= 2 * r by A1, Def8; :: thesis: verum