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 that
A1: Ball x,a meets Ball z,c and
A2: Ball z,c meets Ball y,b ; :: thesis: dist x,y < (a + b) + (2 * c)
A3: (dist x,z) + (dist z,y) < (a + c) + (dist z,y) by A1, Th39, XREAL_1:10;
(a + c) + (dist z,y) < (a + c) + (c + b) by A2, Th39, XREAL_1:10;
then A4: (dist x,z) + (dist z,y) < (a + c) + (c + b) by A3, 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 A4, XXREAL_0:2; :: thesis: verum