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:12;
then A2: (dist t1,x) + (dist t1,y) < r + r by XREAL_1:10;
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 A3: t1 in Ball t1,r by Th16;
Ball t1,r is bounded by Th19;
hence diameter (Ball t1,r) <= 2 * r by A3, A1, Def10; :: thesis: verum