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