theorem :: XREAL_1:176

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