for r, s, s1, s2 being Real
for u being Point of (Euclid 2) st u = |[r,s]| & 0 <= s2 & s2 < s1 holds
|[r,(s - s2)]| in Ball (u,s1)