for E being RealNormSpace
for r being Real
for z, y1, y2 being Point of E st y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) holds
[.y1,y2.] c= cl_Ball (z,r)