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

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

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

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

end;

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

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

end;

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

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 ((1 - d) * b) + (d * c) < a by A4, A5, Lm8; :: thesis: verum

end;

end;