theorem :: TOPREAL6:16

for a, r being Real st r >= 0 holds
a in [.(a - r),(a + r).]