let g, x0, r1 be Real; :: thesis: for r being real number st g = x0 + r1 & abs r1 < r holds
( 0 < r & g in ].(x0 - r),(x0 + r).[ )
let r be real number ; :: thesis: ( g = x0 + r1 & abs r1 < r implies ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) )
assume that
A1: g = x0 + r1 and
A2: abs r1 < r ; :: thesis: ( 0 < r & g in ].(x0 - r),(x0 + r).[ )
thus 0 < r by A2, COMPLEX1:132; :: thesis: g in ].(x0 - r),(x0 + r).[
abs (g - x0) < r by A1, A2;
hence g in ].(x0 - r),(x0 + r).[ by RCOMP_1:8; :: thesis: verum