let a, c be Real; :: thesis: ( c > 0 implies a in ['(a - c),(a + c)'] )
assume c > 0 ; :: thesis: a in ['(a - c),(a + c)']
then A2: ( a - c <= a & a <= a + c ) by XREAL_1:43, XREAL_1:29;
then a in [.(a - c),(a + c).] ;
hence a in ['(a - c),(a + c)'] by INTEGRA5:def 3, XXREAL_0:2, A2; :: thesis: verum