theorem :: XREAL_1:172

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