let d, a, b be real number ; :: thesis: ( 0 <= d & d <= 1 & a <= b implies ((1 - d) * a) + (d * b) <= b )
assume A1: ( 0 <= d & d <= 1 & a <= b ) ; :: thesis: ((1 - d) * a) + (d * b) <= b
then 1 - d >= 0 by Th50;
then (1 - d) * a <= (1 - d) * b by A1, Lm12;
then ((1 - d) * a) + (d * b) <= ((1 - d) * b) + (d * b) by Lm6;
hence ((1 - d) * a) + (d * b) <= b ; :: thesis: verum