A1: ( 0 * w = 0. X & v + (0. X) = v ) by RLVECT_1:23, RLVECT_1:def 7;
( 1 - 0 = 1 & 1 * v = v ) by RLVECT_1:def 11;
then v in LSeg v,w by A1;
hence not LSeg v,w is empty ; :: thesis: LSeg v,w is convex
let u, u9 be Point of X; :: according to RLTOPSP1:def 1 :: thesis: for r being Real st 0 <= r & r <= 1 & u in LSeg v,w & u9 in LSeg v,w holds
(r * u) + ((1 - r) * u9) in LSeg v,w
let r be Real; :: thesis: ( 0 <= r & r <= 1 & u in LSeg v,w & u9 in LSeg v,w implies (r * u) + ((1 - r) * u9) in LSeg v,w )
assume that
A2: 0 <= r and
A3: r <= 1 ; :: thesis: ( not u in LSeg v,w or not u9 in LSeg v,w or (r * u) + ((1 - r) * u9) in LSeg v,w )
A4: 0 <= 1 - r by A3, XREAL_1:50;
assume u in LSeg v,w ; :: thesis: ( not u9 in LSeg v,w or (r * u) + ((1 - r) * u9) in LSeg v,w )
then consider s being Real such that
A5: u = ((1 - s) * v) + (s * w) and
A6: 0 <= s and
A7: s <= 1 ;
A8: r * u = (r * ((1 - s) * v)) + (r * (s * w)) by A5, RLVECT_1:def 8
.= ((r * (1 - s)) * v) + (r * (s * w)) by RLVECT_1:def 10
.= ((r * (1 - s)) * v) + ((r * s) * w) by RLVECT_1:def 10 ;
assume u9 in LSeg v,w ; :: thesis: (r * u) + ((1 - r) * u9) in LSeg v,w
then consider t being Real such that
A9: u9 = ((1 - t) * v) + (t * w) and
A10: 0 <= t and
A11: t <= 1 ;
(1 - r) * u9 = ((1 - r) * ((1 - t) * v)) + ((1 - r) * (t * w)) by A9, RLVECT_1:def 8
.= (((1 - r) * (1 - t)) * v) + ((1 - r) * (t * w)) by RLVECT_1:def 10
.= (((1 - r) * (1 - t)) * v) + (((1 - r) * t) * w) by RLVECT_1:def 10 ;
then A12: (r * u) + ((1 - r) * u9) = ((r * (1 - s)) * v) + (((r * s) * w) + ((((1 - r) * (1 - t)) * v) + (((1 - r) * t) * w))) by A8, RLVECT_1:def 6
.= ((r * (1 - s)) * v) + ((((1 - r) * (1 - t)) * v) + (((r * s) * w) + (((1 - r) * t) * w))) by RLVECT_1:def 6
.= (((r * (1 - s)) * v) + (((1 - r) * (1 - t)) * v)) + (((r * s) * w) + (((1 - r) * t) * w)) by RLVECT_1:def 6
.= (((r * (1 - s)) + ((1 - r) * (1 - t))) * v) + (((r * s) * w) + (((1 - r) * t) * w)) by RLVECT_1:def 9
.= ((1 - ((r * s) + ((1 - r) * t))) * v) + (((r * s) + ((1 - r) * t)) * w) by RLVECT_1:def 9 ;
((1 - r) * t) + (r * s) <= 1 by A2, A3, A7, A11, XREAL_1:176;
hence (r * u) + ((1 - r) * u9) in LSeg v,w by A2, A6, A10, A12, A4; :: thesis: verum