let a, b, d be Real; :: thesis: ( 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) ; :: thesis: d = 0
set s = ((1 - d) * a) + (d * b);
assume d <> 0 ; :: thesis: 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; :: thesis: verum