let n be Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) ) ; :: thesis: 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; :: thesis: verum