let d, a, b be real number ; :: thesis: ( 0 <= d & d <= 1 & a <= b implies a <= ((1 - d) * a) + (d * b) )
assume ( 0 <= d & d <= 1 & a <= b ) ; :: thesis: a <= ((1 - d) * a) + (d * b)
then d * a <= d * b by Lm12;
then ((1 - d) * a) + (d * a) <= ((1 - d) * a) + (d * b) by Lm6;
hence a <= ((1 - d) * a) + (d * b) ; :: thesis: verum