theorem :: XREAL_1:180

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