let a, r be Real; :: 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 ;
A2: a + 0 <= a + r by A1, XREAL_1:7;
reconsider amr = a - r, apr = a + r as Real ;
reconsider X = [.amr,apr.] as Subset of REAL ;
A3: X = { b where b is Real : ( amr <= b & b <= apr ) } by RCOMP_1:def 1;
a - r <= a - 0 by A1, XREAL_1:13;
hence a in [.(a - r),(a + r).] by A3, A2; :: thesis: verum