let g, x0 be Real; :: thesis: for r being real number st g in ].(x0 - r),(x0 + r).[ holds
abs (g - x0) < r
let r be real number ; :: thesis: ( g in ].(x0 - r),(x0 + r).[ implies abs (g - x0) < r )
assume g in ].(x0 - r),(x0 + r).[ ; :: thesis: abs (g - x0) < r
then A1: ex g1 being Real st
( g1 = g & x0 - r < g1 & g1 < x0 + r ) ;

per cases ( x0 <= g or g <= x0 ) ;

suppose A2: x0 <= g ; :: thesis: abs (g - x0) < r

A3: g - x0 < (x0 + r) - x0 by A1, XREAL_1:16;
0 <= g - x0 by A2, XREAL_1:50;
hence abs (g - x0) < r by A3, ABSVALUE:def 1; :: thesis: verum

end;

suppose g <= x0 ; :: thesis: abs (g - x0) < r

then 0 <= x0 - g by XREAL_1:50;
then A4: x0 - g = abs (- (g - x0)) by ABSVALUE:def 1
.= abs (g - x0) by COMPLEX1:138 ;
x0 - g < x0 - (x0 - r) by A1, XREAL_1:17;
hence abs (g - x0) < r by A4; :: thesis: verum

end;

end;