let r1, r2, t be Real; :: thesis:
assume A1: r1 <= r2 ; :: thesis:

per cases by A1, XXREAL_0:1;

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

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

end;

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

end;

suppose A6: r1 < r2 ; :: thesis:

hereby :: thesis:

assume A7: t in [.r1,r2.] ; :: thesis:
take s1 = (r2 - t) / (r2 - r1); :: thesis:
A8: r2 - r1 > 0 by A6, XREAL_1:52;
t <= r2 by A7, XXREAL_1:1;
then 0 <= r2 - t by XREAL_1:50;
hence 0 <= s1 by A8; :: thesis:
r1 <= t by A7, XXREAL_1:1;
then r2 - t <= r2 - r1 by XREAL_1:12;
hence s1 <= 1 by A8, XREAL_1:187; :: thesis:
thus t = (t * (r2 - r1)) / (r2 - r1) by A8, XCMPLX_1:90
.= (((r2 - t) * r1) + ((t - r1) * r2)) / (r2 - r1)
.= (((r2 - t) * r1) / (r2 - r1)) + (((t - r1) * r2) / (r2 - r1)) by XCMPLX_1:63
.= (((r2 - t) * r1) / (r2 - r1)) + (((t - r1) / (r2 - r1)) * r2) by XCMPLX_1:75
.= (((r2 - t) / (r2 - r1)) * r1) + ((((1 * (r2 - r1)) - (r2 - t)) / (r2 - r1)) * r2) by XCMPLX_1:75
.= (s1 * r1) + ((1 - s1) * r2) by A8, XCMPLX_1:128 ; :: thesis:

end;

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

end;