let r, s be Real; :: thesis: for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V
for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for L1, L2 being Linear_Combination of V
for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
let v be VECTOR of V; :: thesis: for L1, L2 being Linear_Combination of V
for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
let L1, L2 be Linear_Combination of V; :: thesis: for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
let p be Real; :: thesis: ( ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v implies ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) )
set rv = ((r * L1) + ((1 - r) * L2)) . v;
set sv = ((s * L1) + ((1 - s) * L2)) . v;
set v1 = L1 . v;
set v2 = L2 . v;
A1: ((r * L1) + ((1 - r) * L2)) . v = ((r * L1) . v) + (((1 - r) * L2) . v) by RLVECT_2:def 12
.= (r * (L1 . v)) + (((1 - r) * L2) . v) by RLVECT_2:def 13
.= (r * (L1 . v)) + ((1 - r) * (L2 . v)) by RLVECT_2:def 13 ;
A2: ((s * L1) + ((1 - s) * L2)) . v = ((s * L1) . v) + (((1 - s) * L2) . v) by RLVECT_2:def 12
.= (s * (L1 . v)) + (((1 - s) * L2) . v) by RLVECT_2:def 13
.= (s * (L1 . v)) + ((1 - s) * (L2 . v)) by RLVECT_2:def 13 ;
assume that
A3: ((r * L1) + ((1 - r) * L2)) . v <= p and
A4: p <= ((s * L1) + ((1 - s) * L2)) . v ; :: thesis: ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )

per cases ( ((r * L1) + ((1 - r) * L2)) . v = ((s * L1) + ((1 - s) * L2)) . v or ((r * L1) + ((1 - r) * L2)) . v <> ((s * L1) + ((1 - s) * L2)) . v ) ;

suppose A6: ((r * L1) + ((1 - r) * L2)) . v = ((s * L1) + ((1 - s) * L2)) . v ; :: thesis: ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )

take rs = r; :: thesis: ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
thus ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) by A3, A4, A6, XXREAL_0:1; :: thesis: verum

end;

suppose ((r * L1) + ((1 - r) * L2)) . v <> ((s * L1) + ((1 - s) * L2)) . v ; :: thesis: ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )

then A7: (((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) <> 0 ;
set y = (p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v));
set x = ((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v));
take rs = (r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) + (s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))); :: thesis: ( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
A8: ( (r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) + (r * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) = r * ((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) & (s * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) + (s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) = s * ((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) ) ;
A9: (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) = (((((s * L1) + ((1 - s) * L2)) . v) - p) + (p - (((r * L1) + ((1 - r) * L2)) . v))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)) by XCMPLX_1:63
.= 1 by A7, XCMPLX_1:60 ;
A10: p - (((r * L1) + ((1 - r) * L2)) . v) >= (((r * L1) + ((1 - r) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) by A3, XREAL_1:11;
thus p = (p * ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)) by A7, XCMPLX_1:90
.= (((((r * L1) + ((1 - r) * L2)) . v) * ((((s * L1) + ((1 - s) * L2)) . v) - p)) + ((((s * L1) + ((1 - s) * L2)) . v) * (p - (((r * L1) + ((1 - r) * L2)) . v)))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))
.= (((((r * L1) + ((1 - r) * L2)) . v) * ((((s * L1) + ((1 - s) * L2)) . v) - p)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + (((((s * L1) + ((1 - s) * L2)) . v) * (p - (((r * L1) + ((1 - r) * L2)) . v))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) by XCMPLX_1:63
.= (((((r * L1) + ((1 - r) * L2)) . v) * ((((s * L1) + ((1 - s) * L2)) . v) - p)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + (((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) * (((s * L1) + ((1 - s) * L2)) . v)) by XCMPLX_1:75
.= ((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) * ((r * (L1 . v)) + ((1 - r) * (L2 . v)))) + (((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) * ((s * (L1 . v)) + ((1 - s) * (L2 . v)))) by A1, A2, XCMPLX_1:75
.= ((rs * (L1 . v)) + (((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) * (L2 . v))) - (rs * (L2 . v))
.= ((rs * (L1 . v)) + (1 * (L2 . v))) - (rs * (L2 . v)) by A9
.= (rs * (L1 . v)) + ((1 - rs) * (L2 . v))
.= (rs * (L1 . v)) + (((1 - rs) * L2) . v) by RLVECT_2:def 13
.= ((rs * L1) . v) + (((1 - rs) * L2) . v) by RLVECT_2:def 13
.= ((rs * L1) + ((1 - rs) * L2)) . v by RLVECT_2:def 12 ; :: thesis: ( ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
A11: ( (((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) >= (((s * L1) + ((1 - s) * L2)) . v) - p & (((s * L1) + ((1 - s) * L2)) . v) - p >= p - p ) by A3, A4, XREAL_1:11, XREAL_1:12;

hereby :: thesis: ( s <= r implies ( s <= rs & rs <= r ) )

assume r <= s ; :: thesis: ( r <= rs & rs <= s )
then ( r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) <= s * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) & r * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) <= s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) ) by A10, A11, XREAL_1:66;
hence ( r <= rs & rs <= s ) by A8, A9, XREAL_1:8; :: thesis: verum

end;

assume A12: s <= r ; :: thesis: ( s <= rs & rs <= r )
then A13: r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) >= s * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) by A11, XREAL_1:66;
(((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) >= p - (((r * L1) + ((1 - r) * L2)) . v) by A4, XREAL_1:11;
then r * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) >= s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) by A10, A12, XREAL_1:66;
hence ( s <= rs & rs <= r ) by A8, A9, A13, XREAL_1:8; :: thesis: verum

end;

end;