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.[ )
assume g in ].(x0 - r),(x0 + r).[ ; :: thesis: g - x0 in ].(- r),r.[
then consider r1 being Real such that
A1: ( g = x0 + r1 & abs r1 < r ) by Th9;
abs (r1 - 0 ) < r by A1;
then r1 in ].(0 - r),(0 + r).[ by RCOMP_1:8;
hence g - x0 in ].(- r),r.[ by A1; :: thesis: verum