theorem NORMSP31: :: NDIFF_8:22

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 being Real st 0 < r1 & z = [x,y] holds
ex r2 being Real st
( 0 < r2 & r2 < r1 & [:(Ball (x,r2)),(Ball (y,r2)):] c= Ball (z,r1) )