let x0, g, r be Real; :: thesis: ( g in ].(x0 - r),(x0 + r).[ implies |.(g - x0).| < r )
assume g in ].(x0 - r),(x0 + r).[ ; :: thesis: |.(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: |.(g - x0).| < r

A3: g - x0 < (x0 + r) - x0 by A1, XREAL_1:14;
0 <= g - x0 by A2, XREAL_1:48;
hence |.(g - x0).| < r by A3, ABSVALUE:def 1; :: thesis: verum

end;

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

then 0 <= x0 - g by XREAL_1:48;
then A4: x0 - g = |.(- (g - x0)).| by ABSVALUE:def 1
.= |.(g - x0).| by COMPLEX1:52 ;
x0 - g < x0 - (x0 - r) by A1, XREAL_1:15;
hence |.(g - x0).| < r by A4; :: thesis: verum

end;

end;