let a, b, c, d be Real; ( 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
; ((1 - d) * b) + (d * c) <= a
1 - d >= 0
by A2, Th48;
then A5:
(1 - d) * a >= (1 - d) * b
by A3, Lm12;
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, Lm6; verum