let a, r be real number ; :: thesis: ( r >= 0 implies a in [.(a - r),(a + r).] )
assume A1: r >= 0 ; :: thesis: a in [.(a - r),(a + r).]
reconsider a = a, r = r as Real by XREAL_0:def 1;
A2: [.(a - r),(a + r).] = { b where b is Real : ( a - r <= b & b <= a + r ) } by RCOMP_1:def 1;
( a - r <= a - 0 & a + 0 <= a + r ) by A1, XREAL_1:9, XREAL_1:15;
hence a in [.(a - r),(a + r).] by A2; :: thesis: verum