for t, r1, r2 being Real st r1 <= r2 holds
( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )