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