let a, b, c, d be Real; :: thesis: ( 0 <= d & d <= 1 & b < a & c < a implies ((1 - d) * b) + (d * c) < a )
assume that
A1: 0 <= d and
A2: d <= 1 and
A3: a > b and
A4: 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 A3; :: thesis: verum

end;

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

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

end;

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

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

end;

end;