theorem :: BORSUK_4:7

for s1, s3, s4, l being Real st s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 holds
s1 <= ((1 - l) * s3) + (l * s4)