let g, x0 be Real; :: thesis: for r being real number st g - x0 in ].(- r),r.[ holds
( 0 < r & g in ].(x0 - r),(x0 + r).[ )
let r be real number ; :: 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 A2: abs (g - x0) < r by SEQ_2:9;
x0 + (g - x0) = g ;
hence ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) by A2, Th11; :: thesis: verum