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 p in LSeg p1,p2 by Def6;
then consider s1 being Real such that
A2: p = ((1 - s1) * p1) + (s1 * p2) and
A3: 0 <= s1 and
A4: s1 <= 1 ;
q in LSeg p1,p2 by A1, Def6;
then consider s2 being Real such that
A5: q = ((1 - s2) * p1) + (s2 * p2) and
A6: 0 <= s2 and
A7: s2 <= 1 ;
A8: s1 <= s2 by A1, A2, A4, A5, A6, A7, Def6;
A9: 1 - s1 >= 0 by A4, XREAL_1:50;
A10: now
per cases ( 1 - s1 <> 0 or 1 - s1 = 0 ) ;
case A11: 1 - s1 <> 0 ; :: thesis: q in LSeg p,p2
set s = (s2 - s1) / (1 - s1);
A12: (1 - s1) * ((1 - s2) / (1 - s1)) = 1 - s2 by A11, XCMPLX_1:88;
A13: (1 - s1) * ((s2 - s1) / (1 - s1)) = s2 - s1 by A11, XCMPLX_1:88;
1 - ((s2 - s1) / (1 - s1)) = ((1 * (1 - s1)) - (s2 - s1)) / (1 - s1) by A11, XCMPLX_1:128
.= (((1 - s1) + s1) - s2) / (1 - s1) ;
then (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 A2, 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 A12, EUCLID:34
.= (((1 - s2) * ((1 - s1) * p1)) + ((1 - s2) * (s1 * p2))) + ((s2 - s1) * p2) by A13, 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 A5, EUCLID:36 ;
then A14: q = ((1 - ((s2 - s1) / (1 - s1))) * p) + (((s2 - s1) / (1 - s1)) * p2) by A11, EUCLID:38;
1 - s1 >= s2 - s1 by A7, XREAL_1:11;
then (1 - s1) / (1 - s1) >= (s2 - s1) / (1 - s1) by A9, XREAL_1:74;
then A15: 1 >= (s2 - s1) / (1 - s1) by A11, XCMPLX_1:60;
s2 - s1 >= 0 by A8, XREAL_1:50;
hence q in LSeg p,p2 by A9, A15, A14; :: thesis: verum
end;
case 1 - s1 = 0 ; :: thesis: q in LSeg p,p2
then s2 = 1 by A7, A8, XXREAL_0:1;
then q = (0. (TOP-REAL 2)) + (1 * p2) by A5, 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 A16: s2 <> 0 ; :: thesis: p in LSeg p1,q
set s = s1 / s2;
s2 / s2 >= s1 / s2 by A6, A8, XREAL_1:74;
then A17: 1 >= s1 / s2 by A16, XCMPLX_1:60;
A18: (s2 - s1) + (s1 * (1 - s2)) = s2 * (1 - s1) ;
A19: s2 * (s1 / s2) = s1 by A16, XCMPLX_1:88;
A20: s2 * ((s2 - s1) / s2) = s2 - s1 by A16, XCMPLX_1:88;
s2 * (((1 - (s1 / s2)) * p1) + ((s1 / s2) * q)) = s2 * (((((1 * s2) - s1) / s2) * p1) + ((s1 / s2) * (((1 - s2) * p1) + (s2 * p2)))) by A5, A16, 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 A20, EUCLID:34
.= ((s2 - s1) * p1) + ((s1 * ((1 - s2) * p1)) + (s1 * (s2 * p2))) by A19, 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 A18, EUCLID:34
.= (s2 * ((1 - s1) * p1)) + (s2 * (s1 * p2)) by EUCLID:34
.= s2 * p by A2, EUCLID:36 ;
then p = ((1 - (s1 / s2)) * p1) + ((s1 / s2) * q) by A16, EUCLID:38;
hence p in LSeg p1,q by A3, A6, A17; :: thesis: verum
end;
case s2 = 0 ; :: thesis: p in LSeg p1,q
then s1 = 0 by A1, A2, A3, A4, A5, Def6;
then p = (1 * p1) + (0. (TOP-REAL 2)) by A2, 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 A10; :: thesis: verum