let d, a, b, c be real number ; :: thesis: ( 0 <= d & d <= 1 & a < b & a < c implies a < ((1 - d) * b) + (d * c) )
assume A1: ( 0 <= d & d <= 1 & a < b & 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 A1; :: thesis: verum

end;

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

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

end;

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

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

end;

end;