theorem Th1: :: JORDAN6:1

for s, r being Real st r <= s holds
( r <= (r + s) / 2 & (r + s) / 2 <= s )