let a, b, d be Real; ( 0 <= d & d <= 1 & a <= ((1 - d) * a) + (d * b) & b < ((1 - d) * a) + (d * b) implies d = 0 )
assume that
A1:
d >= 0
and
A2:
d <= 1
and
A3:
a <= ((1 - d) * a) + (d * b)
and
A4:
b < ((1 - d) * a) + (d * b)
; d = 0
set s = ((1 - d) * a) + (d * b);
assume
d <> 0
; contradiction
then A5:
d * b < d * (((1 - d) * a) + (d * b))
by A1, A4, Lm13;
1 - d >= 0
by A2, Th48;
then A6:
(1 - d) * a <= (1 - d) * (((1 - d) * a) + (d * b))
by A3, Lm12;
1 * (((1 - d) * a) + (d * b)) = ((1 - d) * (((1 - d) * a) + (d * b))) + (d * (((1 - d) * a) + (d * b)))
;
hence
contradiction
by A5, A6, Lm8; verum