for a, b, c being Real holds
( a <= b iff c - b <= c - a )