theorem :: XREAL_1:177

for a, b, c, d being Real st 0 < d & d < 1 & a <= b & a < c holds
a < ((1 - d) * b) + (d * c)