let n be Element of NAT ; :: thesis: for a, b being real number
for x, y being Point of (Euclid n) st Ball x,a meets Ball y,b holds
dist x,y < a + b
let a, b be real number ; :: thesis: for x, y being Point of (Euclid n) st Ball x,a meets Ball y,b holds
dist x,y < a + b
let x, y be Point of (Euclid n); :: thesis: ( Ball x,a meets Ball y,b implies dist x,y < a + b )
assume Ball x,a meets Ball y,b ; :: thesis: dist x,y < a + b
then consider z being set such that
A1: ( z in Ball x,a & z in Ball y,b ) by XBOOLE_0:3;
reconsider z = z as Point of (Euclid n) by A1;
A2: dist x,z < a by A1, METRIC_1:12;
dist y,z < b by A1, METRIC_1:12;
then A3: (dist x,z) + (dist y,z) < (dist x,z) + b by XREAL_1:10;
(dist x,z) + b < a + b by A2, XREAL_1:10;
then A4: (dist x,z) + (dist y,z) < a + b by A3, XXREAL_0:2;
(dist x,z) + (dist y,z) >= dist x,y by METRIC_1:4;
hence dist x,y < a + b by A4, XXREAL_0:2; :: thesis: verum