theorem :: XREAL_1:171

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