set P = halfline p,q;
let u, v be Point of (TOP-REAL n); :: according to JORDAN1:def 1 :: thesis: ( not u in halfline p,q or not v in halfline p,q or LSeg u,v c= halfline p,q )
assume u in halfline p,q ; :: thesis: ( 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 ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg u,v or x in halfline p,q )
assume x in LSeg u,v ; :: thesis: 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);
1 - r >= r - r by A6, XREAL_1:15;
then A8: (1 - r) * a >= 0 * a by A2;
r * b >= 0 * 0 by A4, A5;
then A9: 0 + 0 <= ((1 - r) * a) + (r * b) by A8;
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 A9; :: thesis: verum