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

proof

assume r in ].p,g.[ ; :: thesis: abs ((p + g) - (2 * r)) < g - p
then ex s being Real st
( s = r & p < s & s < g ) ;
then ( 2 * p < 2 * r & 2 * r < 2 * g ) by XREAL_1:70;
then ( - (2 * p) > - (2 * r) & - (2 * r) > - (2 * g) ) by XREAL_1:26;
then ( (p + g) + (- (2 * p)) > (p + g) + (- (2 * r)) & (p + g) + (- (2 * r)) > (p + g) + (- (2 * g)) ) by XREAL_1:8;
then ( g - p > (p + g) - (2 * r) & (p + g) - (2 * r) > - (g - p) ) ;
hence abs ((p + g) - (2 * r)) < g - p by SEQ_2:9; :: thesis: verum

end;

assume abs ((p + g) - (2 * r)) < g - p ; :: thesis: r in ].p,g.[
then A1: ( g - p > (p + g) - (2 * r) & (p + g) - (2 * r) > - (g - p) ) by SEQ_2:9;
then (2 * r) + (g - p) > p + g by XREAL_1:21;
then 2 * r > (p + g) - (g - p) by XREAL_1:21;
then A2: (1 / 2) * (2 * r) > (1 / 2) * (2 * p) by XREAL_1:70;
p + g > (p - g) + (2 * r) by A1, XREAL_1:22;
then (p + g) - (p - g) > 2 * r by XREAL_1:22;
then (1 / 2) * (2 * g) > (1 / 2) * (2 * r) by XREAL_1:70;
hence r in ].p,g.[ by A2; :: thesis: verum