let u, v be Point of V; JORDAN1:def 1 ( not u in halfline (p,q) or not v in halfline (p,q) or LSeg (u,v) c= halfline (p,q) )
set P = halfline (p,q);
assume
u in halfline (p,q)
; ( not v in halfline (p,q) or LSeg (u,v) c= halfline (p,q) )
then consider a being Real such that
A1:
u = ((1 - a) * p) + (a * q)
and
A2:
0 <= a
;
assume
v in halfline (p,q)
; LSeg (u,v) c= halfline (p,q)
then consider b being Real such that
A3:
v = ((1 - b) * p) + (b * q)
and
A4:
0 <= b
;
let x be object ; TARSKI:def 3 ( not x in LSeg (u,v) or x in halfline (p,q) )
assume
x in LSeg (u,v)
; x in halfline (p,q)
then consider r being Real such that
A5:
0 <= r
and
A6:
r <= 1
and
A7:
x = ((1 - r) * u) + (r * v)
by RLTOPSP1:76;
set o = ((1 - r) * a) + (r * b);
A8:
1 - r >= r - r
by A6, XREAL_1:13;
x =
(((1 - r) * ((1 - a) * p)) + ((1 - r) * (a * q))) + (r * (((1 - b) * p) + (b * q)))
by A1, A3, A7, RLVECT_1:def 5
.=
(((1 - r) * ((1 - a) * p)) + ((1 - r) * (a * q))) + ((r * ((1 - b) * p)) + (r * (b * q)))
by RLVECT_1:def 5
.=
(((1 - r) * ((1 - a) * p)) + ((r * ((1 - b) * p)) + (r * (b * q)))) + ((1 - r) * (a * q))
by RLVECT_1:def 3
.=
((((1 - r) * ((1 - a) * p)) + (r * ((1 - b) * p))) + (r * (b * q))) + ((1 - r) * (a * q))
by RLVECT_1:def 3
.=
(((((1 - r) * (1 - a)) * p) + (r * ((1 - b) * p))) + (r * (b * q))) + ((1 - r) * (a * q))
by RLVECT_1:def 7
.=
(((((1 - r) * (1 - a)) * p) + ((r * (1 - b)) * p)) + (r * (b * q))) + ((1 - r) * (a * q))
by RLVECT_1:def 7
.=
(((((1 - r) * (1 - a)) * p) + ((r * (1 - b)) * p)) + ((r * b) * q)) + ((1 - r) * (a * q))
by RLVECT_1:def 7
.=
(((((1 - r) * (1 - a)) * p) + ((r * (1 - b)) * p)) + ((r * b) * q)) + (((1 - r) * a) * q)
by RLVECT_1:def 7
.=
(((((1 - r) * (1 - a)) + (r * (1 - b))) * p) + ((r * b) * q)) + (((1 - r) * a) * q)
by RLVECT_1:def 6
.=
((((1 - r) * (1 - a)) + (r * (1 - b))) * p) + (((r * b) * q) + (((1 - r) * a) * q))
by RLVECT_1:def 3
.=
((1 - (((1 - r) * a) + (r * b))) * p) + ((((1 - r) * a) + (r * b)) * q)
by RLVECT_1:def 6
;
hence
x in halfline (p,q)
by A2, A4, A5, A8; verum