theorem Th9: :: KURATO_2:9

for n being Nat
for a, b being Real
for x, y being Point of (Euclid n) st Ball (x,a) meets Ball (y,b) holds
dist (x,y) < a + b