theorem Th7: :: GOBOARD6:7

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