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