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;

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