let g, r, p be Real; :: thesis: ( r in [.p,g.] iff |.((p + g) - (2 * r)).| <= g - p )
thus ( r in [.p,g.] implies |.((p + g) - (2 * r)).| <= g - p ) :: thesis: ( |.((p + g) - (2 * r)).| <= g - p implies r in [.p,g.] )

proof

assume r in [.p,g.] ; :: thesis: |.((p + g) - (2 * r)).| <= g - p
then A1: ex s being Real st
( s = r & p <= s & s <= g ) ;
then 2 * r <= 2 * g by XREAL_1:64;
then - (2 * r) >= - (2 * g) by XREAL_1:24;
then (p + g) + (- (2 * r)) >= (p + g) + (- (2 * g)) by XREAL_1:7;
then A2: (p + g) - (2 * r) >= - (g - p) ;
2 * p <= 2 * r by A1, XREAL_1:64;
then - (2 * p) >= - (2 * r) by XREAL_1:24;
then (p + g) + (- (2 * p)) >= (p + g) + (- (2 * r)) by XREAL_1:7;
hence |.((p + g) - (2 * r)).| <= g - p by A2, ABSVALUE:5; :: thesis: verum

end;

assume A3: |.((p + g) - (2 * r)).| <= g - p ; :: thesis: r in [.p,g.]
then (p + g) - (2 * r) >= - (g - p) by ABSVALUE:5;
then p + g >= (p - g) + (2 * r) by XREAL_1:19;
then (p + g) - (p - g) >= 2 * r by XREAL_1:19;
then A4: (1 / 2) * (2 * g) >= (1 / 2) * (2 * r) by XREAL_1:64;
g - p >= (p + g) - (2 * r) by A3, ABSVALUE:5;
then (2 * r) + (g - p) >= p + g by XREAL_1:20;
then 2 * r >= (p + g) - (g - p) by XREAL_1:20;
then (1 / 2) * (2 * r) >= (1 / 2) * (2 * p) by XREAL_1:64;
hence r in [.p,g.] by A4; :: thesis: verum