theorem :: TOPREAL3:25

for r, r1, r2, s1, s2 being Real
for u being Point of (Euclid 2) st |[r1,r2]| in Ball (u,r) & |[s1,s2]| in Ball (u,r) & not |[r1,s2]| in Ball (u,r) holds
|[s1,r2]| in Ball (u,r)