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