let x0, r1, g, r be Real; :: thesis: ( g = x0 + r1 & |.r1.| < r implies ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) )
assume that
A1: g = x0 + r1 and
A2: |.r1.| < r ; :: thesis: ( 0 < r & g in ].(x0 - r),(x0 + r).[ )
thus 0 < r by A2, COMPLEX1:46; :: thesis: g in ].(x0 - r),(x0 + r).[
|.(g - x0).| < r by A1, A2;
hence g in ].(x0 - r),(x0 + r).[ by RCOMP_1:1; :: thesis: verum