A1:
( 0 * w = 0. X & v + (0. X) = v )
by RLVECT_1:10;
( 1 - 0 = 1 & 1 * v = v )
by RLVECT_1:def 8;
then
v in LSeg (v,w)
by A1;
hence
not LSeg (v,w) is empty
; LSeg (v,w) is convex
let u, u9 be Point of X; RLTOPSP1:def 1 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; ( 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
; ( 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:48;
assume
u in LSeg (v,w)
; ( 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 5
.=
((r * (1 - s)) * v) + (r * (s * w))
by RLVECT_1:def 7
.=
((r * (1 - s)) * v) + ((r * s) * w)
by RLVECT_1:def 7
;
assume
u9 in LSeg (v,w)
; (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 5
.=
(((1 - r) * (1 - t)) * v) + ((1 - r) * (t * w))
by RLVECT_1:def 7
.=
(((1 - r) * (1 - t)) * v) + (((1 - r) * t) * w)
by RLVECT_1:def 7
;
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 3
.=
((r * (1 - s)) * v) + ((((1 - r) * (1 - t)) * v) + (((r * s) * w) + (((1 - r) * t) * w)))
by RLVECT_1:def 3
.=
(((r * (1 - s)) * v) + (((1 - r) * (1 - t)) * v)) + (((r * s) * w) + (((1 - r) * t) * w))
by RLVECT_1:def 3
.=
(((r * (1 - s)) + ((1 - r) * (1 - t))) * v) + (((r * s) * w) + (((1 - r) * t) * w))
by RLVECT_1:def 6
.=
((1 - ((r * s) + ((1 - r) * t))) * v) + (((r * s) + ((1 - r) * t)) * w)
by RLVECT_1:def 6
;
((1 - r) * t) + (r * s) <= 1
by A2, A3, A7, A11, XREAL_1:174;
hence
(r * u) + ((1 - r) * u9) in LSeg (v,w)
by A2, A6, A10, A12, A4; verum