let a, b, d be Real; :: thesis: ( d <= 1 & a <= b implies ((1 - d) * a) + (d * b) <= b )
assume that
A1: d <= 1 and
A2: a <= b ; :: thesis: ((1 - d) * a) + (d * b) <= b
1 - d >= 0 by A1, Th48;
then (1 - d) * a <= (1 - d) * b by A2, Lm12;
then ((1 - d) * a) + (d * b) <= ((1 - d) * b) + (d * b) by Lm6;
hence ((1 - d) * a) + (d * b) <= b ; :: thesis: verum