let a, b, c be Real; ( a <= b & b < c implies a < (b + c) / 2 )
assume that
A1:
a <= b
and
A2:
b < c
; a < (b + c) / 2
A3:
a + b < b + c
by A1, A2, XREAL_1:8;
a + a <= a + b
by A1, XREAL_1:7;
then
2 * a < b + c
by A3, XXREAL_0:2;
then
(2 * a) / 2 < (b + c) / 2
by XREAL_1:74;
hence
a < (b + c) / 2
; verum