let X be RealUnitarySpace; for x, y, z being Point of X
for r being Real st y in Ball (x,r) & z in Ball (x,r) holds
dist (y,z) < 2 * r
let x, y, z be Point of X; for r being Real st y in Ball (x,r) & z in Ball (x,r) holds
dist (y,z) < 2 * r
let r be Real; ( y in Ball (x,r) & z in Ball (x,r) implies dist (y,z) < 2 * r )
assume that
A1:
y in Ball (x,r)
and
A2:
z in Ball (x,r)
; dist (y,z) < 2 * r
dist (x,z) < r
by A2, Th41;
then A3:
r + (dist (x,z)) < r + r
by XREAL_1:6;
A4:
dist (y,z) <= (dist (y,x)) + (dist (x,z))
by BHSP_1:35;
dist (x,y) < r
by A1, Th41;
then
(dist (x,y)) + (dist (x,z)) < r + (dist (x,z))
by XREAL_1:6;
then
(dist (x,y)) + (dist (x,z)) < 2 * r
by A3, XXREAL_0:2;
hence
dist (y,z) < 2 * r
by A4, XXREAL_0:2; verum