let n be Nat; for a, b, c being Real
for x, y, z being Point of (Euclid n) st Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) holds
dist (x,y) < (a + b) + (2 * c)
let a, b, c be Real; for x, y, z being Point of (Euclid n) st Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) holds
dist (x,y) < (a + b) + (2 * c)
let x, y, z be Point of (Euclid n); ( Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) implies dist (x,y) < (a + b) + (2 * c) )
assume
( Ball (x,a) meets Ball (z,c) & Ball (z,c) meets Ball (y,b) )
; dist (x,y) < (a + b) + (2 * c)
then
( (dist (x,z)) + (dist (z,y)) < (a + c) + (dist (z,y)) & (a + c) + (dist (z,y)) < (a + c) + (c + b) )
by Th9, XREAL_1:8;
then A1:
(dist (x,z)) + (dist (z,y)) < (a + c) + (c + b)
by XXREAL_0:2;
dist (x,y) <= (dist (x,z)) + (dist (z,y))
by METRIC_1:4;
hence
dist (x,y) < (a + b) + (2 * c)
by A1, XXREAL_0:2; verum