theorem Th1: :: RINFSUP1:1
for r, s, t being Real holds
( ( s - r < t & s + r > t ) iff |.(t - s).| < r )