let g, r, p be Real; :: thesis: ( r in ].(p - g),(p + g).[ iff |.(r - p).| < g )
thus ( r in ].(p - g),(p + g).[ implies |.(r - p).| < g ) :: thesis: ( |.(r - p).| < g implies r in ].(p - g),(p + g).[ )
proof
assume r in ].(p - g),(p + g).[ ; :: thesis: |.(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:20;
r - p < g by A1, XREAL_1:19;
hence |.(r - p).| < g by A2, SEQ_2:1; :: thesis: verum
end;
assume A3: |.(r - p).| < g ; :: thesis: r in ].(p - g),(p + g).[
then r - p < g by SEQ_2:1;
then A4: r < p + g by XREAL_1:19;
- g < r - p by A3, SEQ_2:1;
then ( r is Real & p + (- g) < r ) by XREAL_1:20;
hence r in ].(p - g),(p + g).[ by A4; :: thesis: verum