let s1, s3, s4, l be Real; ( s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 implies s1 <= ((1 - l) * s3) + (l * s4) )
assume that
A1:
s1 <= s3
and
A2:
s1 < s4
and
A3:
0 <= l
and
A4:
l <= 1
; s1 <= ((1 - l) * s3) + (l * s4)
hence
s1 <= ((1 - l) * s3) + (l * s4)
; verum