let n be Element of NAT ; :: thesis: for a, b, c being real number
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 number ; :: 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 Th39, XREAL_1:10;
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