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