let g, x0 be Real; :: thesis: for r being real number st g in ].(x0 - r),(x0 + r).[ holds
g - x0 in ].(- r),r.[
let r be real number ; :: 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 abs (g - x0) < r by Th9;
then abs ((g - x0) - 0) < r ;
then g - x0 in ].(0 - r),(0 + r).[ by RCOMP_1:1;
hence g - x0 in ].(- r),r.[ ; :: thesis: verum