theorem Th8: :: COUSIN:7

for a, b being Real st a <= b holds
( a <= (a + b) / 2 & (a + b) / 2 <= b )