let u, v be Point of (TOP-REAL n); 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 number such that
A1:
u = ((1 - a) * p) + (a * q)
and
A2:
0 <= a
by Th26;
assume
v in halfline (p,q)
; LSeg (u,v) c= halfline (p,q)
then consider b being real number such that
A3:
v = ((1 - b) * p) + (b * q)
and
A4:
0 <= b
by Th26;
let x be set ; 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 JGRAPH_1:52;
set o = ((1 - r) * a) + (r * b);
A8:
1 - r >= r - r
by A6, XREAL_1:15;
x =
(((1 - r) * ((1 - a) * p)) + ((1 - r) * (a * q))) + (r * (((1 - b) * p) + (b * q)))
by A1, A3, A7, EUCLID:36
.=
(((1 - r) * ((1 - a) * p)) + ((1 - r) * (a * q))) + ((r * ((1 - b) * p)) + (r * (b * q)))
by EUCLID:36
.=
(((1 - r) * ((1 - a) * p)) + ((r * ((1 - b) * p)) + (r * (b * q)))) + ((1 - r) * (a * q))
by EUCLID:30
.=
((((1 - r) * ((1 - a) * p)) + (r * ((1 - b) * p))) + (r * (b * q))) + ((1 - r) * (a * q))
by EUCLID:30
.=
(((((1 - r) * (1 - a)) * p) + (r * ((1 - b) * p))) + (r * (b * q))) + ((1 - r) * (a * q))
by EUCLID:34
.=
(((((1 - r) * (1 - a)) * p) + ((r * (1 - b)) * p)) + (r * (b * q))) + ((1 - r) * (a * q))
by EUCLID:34
.=
(((((1 - r) * (1 - a)) * p) + ((r * (1 - b)) * p)) + ((r * b) * q)) + ((1 - r) * (a * q))
by EUCLID:34
.=
(((((1 - r) * (1 - a)) * p) + ((r * (1 - b)) * p)) + ((r * b) * q)) + (((1 - r) * a) * q)
by EUCLID:34
.=
(((((1 - r) * (1 - a)) + (r * (1 - b))) * p) + ((r * b) * q)) + (((1 - r) * a) * q)
by EUCLID:37
.=
((((1 - r) * (1 - a)) + (r * (1 - b))) * p) + (((r * b) * q) + (((1 - r) * a) * q))
by EUCLID:30
.=
((1 - (((1 - r) * a) + (r * b))) * p) + ((((1 - r) * a) + (r * b)) * q)
by EUCLID:37
;
hence
x in halfline (p,q)
by A2, A4, A5, A8; verum