let t, r1, r2 be Real; :: thesis: ( r1 <= r2 implies ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) ) )
assume A1: r1 <= r2 ; :: thesis: ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )

per cases ( r1 = r2 or r1 < r2 ) by A1, XXREAL_0:1;

suppose A2: r1 = r2 ; :: thesis: ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )

then A3: [.r1,r2.] = {r1} by XXREAL_1:17;

hereby :: thesis: ( ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) implies t in [.r1,r2.] )

reconsider a19 = 1 as Real ;
assume A4: t in [.r1,r2.] ; :: thesis: ex s being Real st
( 0 <= s & s <= 1 & t = (s * r1) + ((1 - s) * r2) )
take s = a19; :: thesis: ( 0 <= s & s <= 1 & t = (s * r1) + ((1 - s) * r2) )
thus ( 0 <= s & s <= 1 ) ; :: thesis: t = (s * r1) + ((1 - s) * r2)
thus t = (s * r1) + ((1 - s) * r2) by A3, A4, TARSKI:def 1; :: thesis: verum

end;

given s1 being Real such that 0 <= s1 and
s1 <= 1 and
A5: t = (s1 * r1) + ((1 - s1) * r2) ; :: thesis: t in [.r1,r2.]
thus t in [.r1,r2.] by A2, A3, A5, TARSKI:def 1; :: thesis: verum

end;

suppose A6: r1 < r2 ; :: thesis: ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )

hereby :: thesis: ( ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) implies t in [.r1,r2.] )

assume A7: t in [.r1,r2.] ; :: thesis: ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) )
reconsider s1 = (r2 - t) / (r2 - r1) as Real ;
take s1 = s1; :: thesis: ( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) )
A8: r2 - r1 > 0 by A6, XREAL_1:50;
t <= r2 by A7, XXREAL_1:1;
then 0 <= r2 - t by XREAL_1:48;
hence 0 <= s1 by A8; :: thesis: ( s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) )
r1 <= t by A7, XXREAL_1:1;
then r2 - t <= r2 - r1 by XREAL_1:10;
hence s1 <= 1 by A8, XREAL_1:185; :: thesis: t = (s1 * r1) + ((1 - s1) * r2)
thus t = (t * (r2 - r1)) / (r2 - r1) by A8, XCMPLX_1:89
.= (((r2 - t) * r1) + ((t - r1) * r2)) / (r2 - r1)
.= (((r2 - t) * r1) / (r2 - r1)) + (((t - r1) * r2) / (r2 - r1)) by XCMPLX_1:62
.= (((r2 - t) * r1) / (r2 - r1)) + (((t - r1) / (r2 - r1)) * r2) by XCMPLX_1:74
.= (((r2 - t) / (r2 - r1)) * r1) + ((((1 * (r2 - r1)) - (r2 - t)) / (r2 - r1)) * r2) by XCMPLX_1:74
.= (s1 * r1) + ((1 - s1) * r2) by A8, XCMPLX_1:127 ; :: thesis: verum

end;

given s1 being Real such that A9: 0 <= s1 and
A10: s1 <= 1 and
A11: t = (s1 * r1) + ((1 - s1) * r2) ; :: thesis: t in [.r1,r2.]
A12: (s1 * r2) + ((1 - s1) * r2) = 1 * r2 ;
1 - s1 >= 0 by A10, XREAL_1:48;
then A13: (1 - s1) * r1 <= (1 - s1) * r2 by A6, XREAL_1:64;
s1 * r1 <= s1 * r2 by A6, A9, XREAL_1:64;
then A14: t <= r2 by A11, A12, XREAL_1:6;
(s1 * r1) + ((1 - s1) * r1) = 1 * r1 ;
then r1 <= t by A11, A13, XREAL_1:6;
hence t in [.r1,r2.] by A14, XXREAL_1:1; :: thesis: verum

end;

end;