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, Th50;
then A3: (1 - d) * a >= (1 - d) * b by A1, Lm12;
((1 - d) * a) + (d * a) = a ;
hence ((1 - d) * b) + (d * c) <= a by A2, A3, Lm6; :: thesis: verum