let p0, p, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( p0 in LSeg p,q1 & p0 in LSeg p,q2 & p <> p0 & not q1 in LSeg p,q2 implies q2 in LSeg p,q1 )
assume that
A1: p0 in LSeg p,q1 and
A2: p0 in LSeg p,q2 and
A3: p <> p0 ; :: thesis: ( q1 in LSeg p,q2 or q2 in LSeg p,q1 )
consider r being Real such that
A4: p0 = ((1 - r) * p) + (r * q1) and
A5: 0 <= r and
A6: r <= 1 by A1;
A7: 1 - r >= 0 by A6, XREAL_1:50;
A8: p0 - (r * q1) = (1 - r) * p by A4, EUCLID:52;
consider s being Real such that
A9: p0 = ((1 - s) * p) + (s * q2) and
A10: 0 <= s and
A11: s <= 1 by A2;
A12: 1 - s >= 0 by A11, XREAL_1:50;
A13: p0 - (s * q2) = (1 - s) * p by A9, EUCLID:52;
A14: p0 - ((1 - s) * p) = s * q2 by A9, EUCLID:52;
A15: p0 - ((1 - r) * p) = r * q1 by A4, EUCLID:52;

A16: now

assume A17: r <> s ; :: thesis: ( q1 in LSeg p,q2 or q2 in LSeg p,q1 )

now

per cases ( r < s or s < r ) by A17, XXREAL_0:1;

case A18: r < s ; :: thesis: ( q1 in LSeg p,q2 or q2 in LSeg p,q1 )

((1 - r) * p0) - ((1 - r) * ((1 - s) * p)) = (1 - r) * (s * q2) by A14, EUCLID:53;
then ((1 - r) * p0) - (((1 - r) * (1 - s)) * p) = (1 - r) * (s * q2) by EUCLID:34;
then ((1 - r) * p0) - (((1 - r) * (1 - s)) * p) = ((1 - r) * s) * q2 by EUCLID:34;
then ((1 - r) * p0) - ((1 - s) * ((1 - r) * p)) = ((1 - r) * s) * q2 by EUCLID:34;
then ((1 - r) * p0) - (((1 - s) * p0) - ((1 - s) * (r * q1))) = ((1 - r) * s) * q2 by A8, EUCLID:53;
then (((1 - r) * p0) - ((1 - s) * p0)) + ((1 - s) * (r * q1)) = ((1 - r) * s) * q2 by EUCLID:51;
then A19: (((1 - r) - (1 - s)) * p0) + ((1 - s) * (r * q1)) = ((1 - r) * s) * q2 by EUCLID:54;

A20: now

assume (1 - r) * s = 0 ; :: thesis: contradiction
then A21: ( (1 - r) + r = 0 + r or s = 0 ) by XCMPLX_1:6;

now

per cases ( r = 1 or s = 0 ) by A21;

case r = 1 ; :: thesis: contradiction

hence contradiction by A11, A18; :: thesis: verum

end;

case s = 0 ; :: thesis: contradiction

hence contradiction by A5, A18; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then 1 = ((1 - r) * s) / ((1 - r) * s) by XCMPLX_1:60;
then 1 = ((1 - r) * s) * (((1 - r) * s) " ) by XCMPLX_0:def 9;
then (((1 - r) * s) * (((1 - r) * s) " )) * (((s - r) * p0) + ((1 - s) * (r * q1))) = ((1 - r) * s) * q2 by A19, EUCLID:33;
then ((1 - r) * s) * ((((1 - r) * s) " ) * (((s - r) * p0) + ((1 - s) * (r * q1)))) = ((1 - r) * s) * q2 by EUCLID:34;
then q2 = (((1 - r) * s) " ) * (((s - r) * p0) + ((1 - s) * (r * q1))) by A20, EUCLID:38;
then q2 = (((1 - r) * s) " ) * (((s - r) * p0) + (((1 - s) * r) * q1)) by EUCLID:34;
then q2 = ((((1 - r) * s) " ) * ((s - r) * p0)) + ((((1 - r) * s) " ) * (((1 - s) * r) * q1)) by EUCLID:36;
then q2 = (((((1 - r) * s) " ) * (s - r)) * p0) + ((((1 - r) * s) " ) * (((1 - s) * r) * q1)) by EUCLID:34;
then A22: q2 = (((((1 - r) * s) " ) * (s - r)) * p0) + (((((1 - r) * s) " ) * ((1 - s) * r)) * q1) by EUCLID:34;
set s1 = (((1 - r) * s) " ) * ((1 - s) * r);
q1 in LSeg p,q1 by RLTOPSP1:69;
then A23: LSeg p0,q1 c= LSeg p,q1 by A1, TOPREAL1:12;
(r - (s * r)) + (s * r) <= (s - (s * r)) + (s * r) by A18;
then (1 * r) - (s * r) <= (1 - r) * s by XREAL_1:8;
then (((1 - s) * r) / ((1 - r) * s)) * ((1 - r) * s) <= 1 * ((1 - r) * s) by A20, XCMPLX_1:88;
then ((1 - s) * r) / ((1 - r) * s) <= 1 by A10, A7, A20, XREAL_1:70;
then A24: (((1 - r) * s) " ) * ((1 - s) * r) <= 1 by XCMPLX_0:def 9;
(((1 - r) * s) " ) * (s - r) = (((1 - r) * s) - (((1 - r) * s) - (s - r))) / ((1 - r) * s) by XCMPLX_0:def 9
.= (((1 - r) * s) / ((1 - r) * s)) - ((((1 - r) * s) - (s - r)) / ((1 - r) * s)) by XCMPLX_1:121
.= 1 - (((r + (s - (r * s))) - s) / ((1 - r) * s)) by A20, XCMPLX_1:60
.= 1 - ((((1 - r) * s) " ) * ((1 - s) * r)) by XCMPLX_0:def 9 ;
then q2 in LSeg p0,q1 by A5, A10, A7, A12, A22, A24;
hence ( q1 in LSeg p,q2 or q2 in LSeg p,q1 ) by A23; :: thesis: verum

end;

case A25: s < r ; :: thesis: ( q1 in LSeg p,q2 or q2 in LSeg p,q1 )

((1 - s) * p0) - ((1 - s) * ((1 - r) * p)) = (1 - s) * (r * q1) by A15, EUCLID:53;
then ((1 - s) * p0) - (((1 - s) * (1 - r)) * p) = (1 - s) * (r * q1) by EUCLID:34;
then ((1 - s) * p0) - (((1 - s) * (1 - r)) * p) = ((1 - s) * r) * q1 by EUCLID:34;
then ((1 - s) * p0) - ((1 - r) * ((1 - s) * p)) = ((1 - s) * r) * q1 by EUCLID:34;
then ((1 - s) * p0) - (((1 - r) * p0) - ((1 - r) * (s * q2))) = ((1 - s) * r) * q1 by A13, EUCLID:53;
then (((1 - s) * p0) - ((1 - r) * p0)) + ((1 - r) * (s * q2)) = ((1 - s) * r) * q1 by EUCLID:51;
then A26: (((1 - s) - (1 - r)) * p0) + ((1 - r) * (s * q2)) = ((1 - s) * r) * q1 by EUCLID:54;

A27: now

assume (1 - s) * r = 0 ; :: thesis: contradiction
then A28: ( (1 - s) + s = 0 + s or r = 0 ) by XCMPLX_1:6;

now

per cases ( s = 1 or r = 0 ) by A28;

case s = 1 ; :: thesis: contradiction

hence contradiction by A6, A25; :: thesis: verum

end;

case r = 0 ; :: thesis: contradiction

hence contradiction by A10, A25; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then 1 = ((1 - s) * r) / ((1 - s) * r) by XCMPLX_1:60;
then 1 = ((1 - s) * r) * (((1 - s) * r) " ) by XCMPLX_0:def 9;
then (((1 - s) * r) * (((1 - s) * r) " )) * (((r - s) * p0) + ((1 - r) * (s * q2))) = ((1 - s) * r) * q1 by A26, EUCLID:33;
then ((1 - s) * r) * ((((1 - s) * r) " ) * (((r - s) * p0) + ((1 - r) * (s * q2)))) = ((1 - s) * r) * q1 by EUCLID:34;
then q1 = (((1 - s) * r) " ) * (((r - s) * p0) + ((1 - r) * (s * q2))) by A27, EUCLID:38;
then q1 = (((1 - s) * r) " ) * (((r - s) * p0) + (((1 - r) * s) * q2)) by EUCLID:34;
then q1 = ((((1 - s) * r) " ) * ((r - s) * p0)) + ((((1 - s) * r) " ) * (((1 - r) * s) * q2)) by EUCLID:36;
then q1 = (((((1 - s) * r) " ) * (r - s)) * p0) + ((((1 - s) * r) " ) * (((1 - r) * s) * q2)) by EUCLID:34;
then A29: q1 = (((((1 - s) * r) " ) * (r - s)) * p0) + (((((1 - s) * r) " ) * ((1 - r) * s)) * q2) by EUCLID:34;
set s1 = (((1 - s) * r) " ) * ((1 - r) * s);
q2 in LSeg p,q2 by RLTOPSP1:69;
then A30: LSeg p0,q2 c= LSeg p,q2 by A2, TOPREAL1:12;
(s - (r * s)) + (r * s) <= (r - (r * s)) + (r * s) by A25;
then (1 * s) - (r * s) <= (1 - s) * r by XREAL_1:8;
then (((1 - r) * s) / ((1 - s) * r)) * ((1 - s) * r) <= 1 * ((1 - s) * r) by A27, XCMPLX_1:88;
then ((1 - r) * s) / ((1 - s) * r) <= 1 by A5, A12, A27, XREAL_1:70;
then A31: (((1 - s) * r) " ) * ((1 - r) * s) <= 1 by XCMPLX_0:def 9;
(((1 - s) * r) " ) * (r - s) = (((1 - s) * r) - (((1 - s) * r) - (r - s))) / ((1 - s) * r) by XCMPLX_0:def 9
.= (((1 - s) * r) / ((1 - s) * r)) - ((((1 - s) * r) - (r - s)) / ((1 - s) * r)) by XCMPLX_1:121
.= 1 - (((s + (r - (s * r))) - r) / ((1 - s) * r)) by A27, XCMPLX_1:60
.= 1 - ((((1 - s) * r) " ) * ((1 - r) * s)) by XCMPLX_0:def 9 ;
then q1 in LSeg p0,q2 by A5, A10, A7, A12, A29, A31;
hence ( q1 in LSeg p,q2 or q2 in LSeg p,q1 ) by A30; :: thesis: verum

end;

end;

end;

hence ( q1 in LSeg p,q2 or q2 in LSeg p,q1 ) ; :: thesis: verum

end;

now

assume r = s ; :: thesis: ( q1 in LSeg p,q2 or q2 in LSeg p,q1 )
then (r * q1) + (((1 - r) * p) - ((1 - r) * p)) = ((r * q2) + ((1 - r) * p)) - ((1 - r) * p) by A4, A9, EUCLID:49;
then (r * q1) + (0. (TOP-REAL 2)) = ((r * q2) + ((1 - r) * p)) - ((1 - r) * p) by EUCLID:46;
then (r * q1) + (0. (TOP-REAL 2)) = r * q2 by EUCLID:52;
then A32: r * q1 = r * q2 by EUCLID:31;
A33: q1 in LSeg p,q1 by RLTOPSP1:69;

now

per cases ( r <> 0 or r = 0 ) ;

case r <> 0 ; :: thesis: ( q1 in LSeg p,q2 or q2 in LSeg p,q1 )

hence ( q1 in LSeg p,q2 or q2 in LSeg p,q1 ) by A32, A33, EUCLID:38; :: thesis: verum

end;

case r = 0 ; :: thesis: contradiction

then p0 = ((1 - 0 ) * p) + (0. (TOP-REAL 2)) by A4, EUCLID:33;
then p0 = (1 - 0 ) * p by EUCLID:31;
hence contradiction by A3, EUCLID:33; :: thesis: verum

end;

end;

end;

hence ( q1 in LSeg p,q2 or q2 in LSeg p,q1 ) ; :: thesis: verum

end;

hence ( q1 in LSeg p,q2 or q2 in LSeg p,q1 ) by A16; :: thesis: verum