let s1, s3, s4, l be real number ; :: thesis: ( s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 implies s1 <= ((1 - l) * s3) + (l * s4) )
assume A1: ( s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 ) ; :: thesis: s1 <= ((1 - l) * s3) + (l * s4)

now

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

suppose l = 0 ; :: thesis: s1 <= ((1 - l) * s3) + (l * s4)

hence s1 <= ((1 - l) * s3) + (l * s4) by A1; :: thesis: verum

end;

suppose l = 1 ; :: thesis: s1 <= ((1 - l) * s3) + (l * s4)

hence s1 <= ((1 - l) * s3) + (l * s4) by A1; :: thesis: verum

end;

suppose A2: ( not l = 0 & not l = 1 ) ; :: thesis: s1 <= ((1 - l) * s3) + (l * s4)

then A3: ( l > 0 & l < 1 ) by A1, XXREAL_0:1;
A4: l * s1 < l * s4 by A1, A2, XREAL_1:70;
1 - l > 0 by A3, XREAL_1:52;
then A5: (1 - l) * s1 <= (1 - l) * s3 by A1, XREAL_1:66;
((1 - l) * s1) + (l * s1) = 1 * s1 ;
hence s1 <= ((1 - l) * s3) + (l * s4) by A4, A5, XREAL_1:10; :: thesis: verum

end;

end;

end;

hence s1 <= ((1 - l) * s3) + (l * s4) ; :: thesis: verum