theorem :: RCOMP_1:2

for g, r, p being Real holds
( r in [.p,g.] iff |.((p + g) - (2 * r)).| <= g - p )