theorem :: TOPREAL3:23

for r, r1, s, s1 being Real
for u being Point of (Euclid 2) st |[s,r1]| in Ball (u,r) & |[s,s1]| in Ball (u,r) holds
|[s,((r1 + s1) / 2)]| in Ball (u,r)