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