for r, s, a, b being Real st r in [.a,b.] & s in [.a,b.] holds
(r + s) / 2 in [.a,b.]