let x0, g, r be Real; :: thesis: ( g in ].(x0 - r),(x0 + r).[ implies g - x0 in ].(- r),r.[ )
set r1 = g - x0;
assume g in ].(x0 - r),(x0 + r).[ ; :: thesis: g - x0 in ].(- r),r.[
then |.(g - x0).| < r by Th1;
then |.((g - x0) - 0).| < r ;
then g - x0 in ].(0 - r),(0 + r).[ by RCOMP_1:1;
hence g - x0 in ].(- r),r.[ ; :: thesis: verum