let p, q, p1, p2 be Point of (TOP-REAL 2); :: thesis: ( LE p,q,p1,p2 implies ( q in LSeg p,p2 & p in LSeg p1,q ) )
assume A1: LE p,q,p1,p2 ; :: thesis: ( q in LSeg p,p2 & p in LSeg p1,q )
then A2: ( p in LSeg p1,p2 & q in LSeg p1,p2 & ( for r1, r2 being Real st 0 <= r1 & r1 <= 1 & p = ((1 - r1) * p1) + (r1 * p2) & 0 <= r2 & r2 <= 1 & q = ((1 - r2) * p1) + (r2 * p2) holds
r1 <= r2 ) ) by Def6;
then consider s1 being Real such that
A3: ( p = ((1 - s1) * p1) + (s1 * p2) & 0 <= s1 & s1 <= 1 ) ;
consider s2 being Real such that
A4: ( q = ((1 - s2) * p1) + (s2 * p2) & 0 <= s2 & s2 <= 1 ) by A2;
A5: s1 <= s2 by A1, A3, A4, Def6;
A6: 1 - s1 >= 0 by A3, XREAL_1:50;

A7: now

per cases ( 1 - s1 <> 0 or 1 - s1 = 0 ) ;

case A8: 1 - s1 <> 0 ; :: thesis: q in LSeg p,p2

A9: s2 - s1 >= 0 by A5, XREAL_1:50;
set s = (s2 - s1) / (1 - s1);
A10: (s2 - s1) / (1 - s1) >= 0 by A6, A9;
A11: (1 - s1) * ((1 - s2) / (1 - s1)) = 1 - s2 by A8, XCMPLX_1:88;
A12: (1 - s1) * ((s2 - s1) / (1 - s1)) = s2 - s1 by A8, XCMPLX_1:88;
A13: 1 - ((s2 - s1) / (1 - s1)) = ((1 * (1 - s1)) - (s2 - s1)) / (1 - s1) by A8, XCMPLX_1:128
.= (((1 - s1) + s1) - s2) / (1 - s1) ;
1 - s1 >= s2 - s1 by A4, XREAL_1:11;
then (1 - s1) / (1 - s1) >= (s2 - s1) / (1 - s1) by A6, XREAL_1:74;
then A14: 1 >= (s2 - s1) / (1 - s1) by A8, XCMPLX_1:60;
(1 - s1) * (((1 - ((s2 - s1) / (1 - s1))) * p) + (((s2 - s1) / (1 - s1)) * p2)) = ((1 - s1) * (((1 - s2) / (1 - s1)) * (((1 - s1) * p1) + (s1 * p2)))) + ((1 - s1) * (((s2 - s1) / (1 - s1)) * p2)) by A3, A13, EUCLID:36
.= (((1 - s1) * ((1 - s2) / (1 - s1))) * (((1 - s1) * p1) + (s1 * p2))) + ((1 - s1) * (((s2 - s1) / (1 - s1)) * p2)) by EUCLID:34
.= ((1 - s2) * (((1 - s1) * p1) + (s1 * p2))) + (((1 - s1) * ((s2 - s1) / (1 - s1))) * p2) by A11, EUCLID:34
.= (((1 - s2) * ((1 - s1) * p1)) + ((1 - s2) * (s1 * p2))) + ((s2 - s1) * p2) by A12, EUCLID:36
.= ((((1 - s2) * (1 - s1)) * p1) + ((1 - s2) * (s1 * p2))) + ((s2 - s1) * p2) by EUCLID:34
.= ((((1 - s2) * (1 - s1)) * p1) + (((1 - s2) * s1) * p2)) + ((s2 - s1) * p2) by EUCLID:34
.= (((1 - s2) * (1 - s1)) * p1) + ((((1 - s2) * s1) * p2) + ((s2 - s1) * p2)) by EUCLID:30
.= (((1 - s2) * (1 - s1)) * p1) + ((((1 * s1) - (s2 * s1)) + (s2 - s1)) * p2) by EUCLID:37
.= ((1 - s1) * ((1 - s2) * p1)) + (((1 - s1) * s2) * p2) by EUCLID:34
.= ((1 - s1) * ((1 - s2) * p1)) + ((1 - s1) * (s2 * p2)) by EUCLID:34
.= (1 - s1) * q by A4, EUCLID:36 ;
then q = ((1 - ((s2 - s1) / (1 - s1))) * p) + (((s2 - s1) / (1 - s1)) * p2) by A8, EUCLID:38;
hence q in LSeg p,p2 by A10, A14; :: thesis: verum

end;

case 1 - s1 = 0 ; :: thesis: q in LSeg p,p2

then s2 = 1 by A4, A5, XXREAL_0:1;
then q = (0. (TOP-REAL 2)) + (1 * p2) by A4, EUCLID:33
.= (0. (TOP-REAL 2)) + p2 by EUCLID:33
.= p2 by EUCLID:31 ;
hence q in LSeg p,p2 by RLTOPSP1:69; :: thesis: verum

end;

end;

end;

now

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

case A15: s2 <> 0 ; :: thesis: p in LSeg p1,q

set s = s1 / s2;
A16: s1 / s2 >= 0 by A3, A4;
A17: s2 * ((s2 - s1) / s2) = s2 - s1 by A15, XCMPLX_1:88;
A18: s2 * (s1 / s2) = s1 by A15, XCMPLX_1:88;
A19: (s2 - s1) + (s1 * (1 - s2)) = s2 * (1 - s1) ;
s2 / s2 >= s1 / s2 by A4, A5, XREAL_1:74;
then A20: 1 >= s1 / s2 by A15, XCMPLX_1:60;
s2 * (((1 - (s1 / s2)) * p1) + ((s1 / s2) * q)) = s2 * (((((1 * s2) - s1) / s2) * p1) + ((s1 / s2) * (((1 - s2) * p1) + (s2 * p2)))) by A4, A15, XCMPLX_1:128
.= (s2 * (((s2 - s1) / s2) * p1)) + (s2 * ((s1 / s2) * (((1 - s2) * p1) + (s2 * p2)))) by EUCLID:36
.= ((s2 * ((s2 - s1) / s2)) * p1) + (s2 * ((s1 / s2) * (((1 - s2) * p1) + (s2 * p2)))) by EUCLID:34
.= ((s2 - s1) * p1) + ((s2 * (s1 / s2)) * (((1 - s2) * p1) + (s2 * p2))) by A17, EUCLID:34
.= ((s2 - s1) * p1) + ((s1 * ((1 - s2) * p1)) + (s1 * (s2 * p2))) by A18, EUCLID:36
.= ((s2 - s1) * p1) + (((s1 * (1 - s2)) * p1) + (s1 * (s2 * p2))) by EUCLID:34
.= ((s2 - s1) * p1) + (((s1 * (1 - s2)) * p1) + ((s1 * s2) * p2)) by EUCLID:34
.= (((s2 - s1) * p1) + ((s1 * (1 - s2)) * p1)) + ((s1 * s2) * p2) by EUCLID:30
.= (((s2 - s1) + (s1 * (1 - s2))) * p1) + ((s1 * s2) * p2) by EUCLID:37
.= (s2 * ((1 - s1) * p1)) + ((s2 * s1) * p2) by A19, EUCLID:34
.= (s2 * ((1 - s1) * p1)) + (s2 * (s1 * p2)) by EUCLID:34
.= s2 * p by A3, EUCLID:36 ;
then p = ((1 - (s1 / s2)) * p1) + ((s1 / s2) * q) by A15, EUCLID:38;
hence p in LSeg p1,q by A16, A20; :: thesis: verum

end;

case s2 = 0 ; :: thesis: p in LSeg p1,q

then s1 = 0 by A1, A3, A4, Def6;
then p = (1 * p1) + (0. (TOP-REAL 2)) by A3, EUCLID:33
.= p1 + (0. (TOP-REAL 2)) by EUCLID:33
.= p1 by EUCLID:31 ;
hence p in LSeg p1,q by RLTOPSP1:69; :: thesis: verum

end;

end;

end;

hence ( q in LSeg p,p2 & p in LSeg p1,q ) by A7; :: thesis: verum