let a, b, c, d be Real; :: thesis: ( 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 ; :: thesis: a < ((1 - d) * b) + (d * c)

per cases ( d = 0 or d = 1 or ( not d = 0 & not d = 1 ) ) ;

suppose d = 0 ; :: thesis: a < ((1 - d) * b) + (d * c)

hence a < ((1 - d) * b) + (d * c) by A3; :: thesis: verum

end;

suppose d = 1 ; :: thesis: a < ((1 - d) * b) + (d * c)

hence a < ((1 - d) * b) + (d * c) by A4; :: thesis: verum

end;

suppose A5: ( not d = 0 & not d = 1 ) ; :: thesis: a < ((1 - d) * b) + (d * c)

then d < 1 by A2, XXREAL_0:1;
then 1 - d > 0 by Lm21;
then A6: (1 - d) * a < (1 - d) * b by A3, Lm13;
A7: ((1 - d) * a) + (d * a) = a ;
d * a < d * c by A1, A4, A5, Lm13;
hence a < ((1 - d) * b) + (d * c) by A6, A7, Lm8; :: thesis: verum

end;

end;