theorem Th1: :: RCOMP_1:1

for g, r, p being Real holds
( r in ].(p - g),(p + g).[ iff |.(r - p).| < g )