theorem Th1: :: GOBOARD7:1

for s, r1, r2 being Real holds
( not |.(r1 - r2).| > s or r1 + s < r2 or r2 + s < r1 )