let x0, g, r be Real; :: thesis: ( g - x0 in ].(- r),r.[ implies ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) )
set r1 = g - x0;
assume g - x0 in ].(- r),r.[ ; :: thesis: ( 0 < r & g in ].(x0 - r),(x0 + r).[ )
then ex g1 being Real st
( g1 = g - x0 & - r < g1 & g1 < r ) ;
then A1: |.(g - x0).| < r by SEQ_2:1;
x0 + (g - x0) = g ;
hence ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) by A1, Th3; :: thesis: verum