let r, p, g be real number ; :: thesis: ( r in ].(p - g),(p + g).[ iff abs (r - p) < g )
thus ( r in ].(p - g),(p + g).[ implies abs (r - p) < g ) :: thesis: ( abs (r - p) < g implies r in ].(p - g),(p + g).[ )

proof

assume r in ].(p - g),(p + g).[ ; :: thesis: abs (r - p) < g
then A1: ex s being Real st
( r = s & p - g < s & s < p + g ) ;
then p + (- g) < r ;
then A2: - g < r - p by XREAL_1:22;
r - p < g by A1, XREAL_1:21;
hence abs (r - p) < g by A2, SEQ_2:9; :: thesis: verum

end;

A3: r is Real by XREAL_0:def 1;
assume abs (r - p) < g ; :: thesis: r in ].(p - g),(p + g).[
then A4: ( - g < r - p & r - p < g ) by SEQ_2:9;
then A5: p + (- g) < r by XREAL_1:22;
r < p + g by A4, XREAL_1:21;
hence r in ].(p - g),(p + g).[ by A3, A5; :: thesis: verum