let d, a, b, c be real number ; :: thesis: ( 0 < d & d < 1 & a <= b & a < c implies a < ((1 - d) * b) + (d * c) )
assume A1: ( 0 < d & d < 1 & a <= b & a < c ) ; :: thesis: a < ((1 - d) * b) + (d * c)
then A2: d * a < d * c by Lm13;
1 - d > 0 by A1, Lm21;
then A3: (1 - d) * a <= (1 - d) * b by A1, Lm12;
((1 - d) * a) + (d * a) = a ;
hence a < ((1 - d) * b) + (d * c) by A2, A3, Lm8; :: thesis: verum