let a, b, c, d be Real; ( 0 < d & d < 1 & a <= b & a < c implies a < ((1 - d) * b) + (d * c) )
assume that
A1:
0 < d
and
A2:
d < 1
and
A3:
a <= b
and
A4:
a < c
; a < ((1 - d) * b) + (d * c)
1 - d > 0
by A2, Lm21;
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, Lm13;
hence
a < ((1 - d) * b) + (d * c)
by A5, A6, Lm8; verum