theorem :: TOPREAL3:24

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