theorem Th9: :: GOBOARD6:9

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)