let T be non empty Reflexive symmetric triangle MetrStruct ; 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; for r being Real st 0 < r holds
diameter (Ball (t1,r)) <= 2 * r
let r be Real; ( 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;
( 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) )
;
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;
verum
end;
assume
0 < r
; diameter (Ball (t1,r)) <= 2 * r
then
t1 in Ball (t1,r)
by Th11;
hence
diameter (Ball (t1,r)) <= 2 * r
by A1, Def8; verum