theorem :: COUSIN:8

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