theorem Th2: :: NDIFF10:2

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:]
for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )