let a, r be Real; :: thesis: ( r > 0 implies a in ].(a - r),(a + r).[ )
assume r > 0 ; :: thesis: a in ].(a - r),(a + r).[
then |.(a - a).| < r by ABSVALUE:def 1;
hence a in ].(a - r),(a + r).[ by RCOMP_1:1; :: thesis: verum