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

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

suppose x0 <= g ; :: thesis: abs r1 < r

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

end;

suppose g <= x0 ; :: thesis: abs r1 < r

then 0 <= x0 - g by XREAL_1:50;
then A3: 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 r1 < r by A3; :: thesis: verum

end;

end;