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) ;
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;
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;
A9: 1 - s1 >= 0 by A4, XREAL_1:48;
A10: now :: thesis: ( ( 1 - s1 <> 0 & q in LSeg (p,p2) ) or ( 1 - s1 = 0 & q in LSeg (p,p2) ) )
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:87;
A13: (1 - s1) * ((s2 - s1) / (1 - s1)) = s2 - s1 by A11, XCMPLX_1:87;
1 - ((s2 - s1) / (1 - s1)) = ((1 * (1 - s1)) - (s2 - s1)) / (1 - s1) by A11, XCMPLX_1:127
.= (((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, RLVECT_1:def 5
.= (((1 - s1) * ((1 - s2) / (1 - s1))) * (((1 - s1) * p1) + (s1 * p2))) + ((1 - s1) * (((s2 - s1) / (1 - s1)) * p2)) by RLVECT_1:def 7
.= ((1 - s2) * (((1 - s1) * p1) + (s1 * p2))) + (((1 - s1) * ((s2 - s1) / (1 - s1))) * p2) by A12, RLVECT_1:def 7
.= (((1 - s2) * ((1 - s1) * p1)) + ((1 - s2) * (s1 * p2))) + ((s2 - s1) * p2) by A13, RLVECT_1:def 5
.= ((((1 - s2) * (1 - s1)) * p1) + ((1 - s2) * (s1 * p2))) + ((s2 - s1) * p2) by RLVECT_1:def 7
.= ((((1 - s2) * (1 - s1)) * p1) + (((1 - s2) * s1) * p2)) + ((s2 - s1) * p2) by RLVECT_1:def 7
.= (((1 - s2) * (1 - s1)) * p1) + ((((1 - s2) * s1) * p2) + ((s2 - s1) * p2)) by RLVECT_1:def 3
.= (((1 - s2) * (1 - s1)) * p1) + ((((1 * s1) - (s2 * s1)) + (s2 - s1)) * p2) by RLVECT_1:def 6
.= ((1 - s1) * ((1 - s2) * p1)) + (((1 - s1) * s2) * p2) by RLVECT_1:def 7
.= ((1 - s1) * ((1 - s2) * p1)) + ((1 - s1) * (s2 * p2)) by RLVECT_1:def 7
.= (1 - s1) * q by A5, RLVECT_1:def 5 ;
then A14: q = ((1 - ((s2 - s1) / (1 - s1))) * p) + (((s2 - s1) / (1 - s1)) * p2) by A11, RLVECT_1:36;
1 - s1 >= s2 - s1 by A7, XREAL_1:9;
then (1 - s1) / (1 - s1) >= (s2 - s1) / (1 - s1) by A9, XREAL_1:72;
then A15: 1 >= (s2 - s1) / (1 - s1) by A11, XCMPLX_1:60;
s2 - s1 >= 0 by A8, XREAL_1:48;
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, RLVECT_1:10
.= (0. (TOP-REAL 2)) + p2 by RLVECT_1:def 8
.= p2 by RLVECT_1:4 ;
hence q in LSeg (p,p2) by RLTOPSP1:68; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( s2 <> 0 & p in LSeg (p1,q) ) or ( s2 = 0 & p in LSeg (p1,q) ) )
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:72;
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:87;
A20: s2 * ((s2 - s1) / s2) = s2 - s1 by A16, XCMPLX_1:87;
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:127
.= (s2 * (((s2 - s1) / s2) * p1)) + (s2 * ((s1 / s2) * (((1 - s2) * p1) + (s2 * p2)))) by RLVECT_1:def 5
.= ((s2 * ((s2 - s1) / s2)) * p1) + (s2 * ((s1 / s2) * (((1 - s2) * p1) + (s2 * p2)))) by RLVECT_1:def 7
.= ((s2 - s1) * p1) + ((s2 * (s1 / s2)) * (((1 - s2) * p1) + (s2 * p2))) by A20, RLVECT_1:def 7
.= ((s2 - s1) * p1) + ((s1 * ((1 - s2) * p1)) + (s1 * (s2 * p2))) by A19, RLVECT_1:def 5
.= ((s2 - s1) * p1) + (((s1 * (1 - s2)) * p1) + (s1 * (s2 * p2))) by RLVECT_1:def 7
.= ((s2 - s1) * p1) + (((s1 * (1 - s2)) * p1) + ((s1 * s2) * p2)) by RLVECT_1:def 7
.= (((s2 - s1) * p1) + ((s1 * (1 - s2)) * p1)) + ((s1 * s2) * p2) by RLVECT_1:def 3
.= (((s2 - s1) + (s1 * (1 - s2))) * p1) + ((s1 * s2) * p2) by RLVECT_1:def 6
.= (s2 * ((1 - s1) * p1)) + ((s2 * s1) * p2) by A18, RLVECT_1:def 7
.= (s2 * ((1 - s1) * p1)) + (s2 * (s1 * p2)) by RLVECT_1:def 7
.= s2 * p by A2, RLVECT_1:def 5 ;
then p = ((1 - (s1 / s2)) * p1) + ((s1 / s2) * q) by A16, RLVECT_1:36;
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;
then p = (1 * p1) + (0. (TOP-REAL 2)) by A2, RLVECT_1:10
.= p1 + (0. (TOP-REAL 2)) by RLVECT_1:def 8
.= p1 by RLVECT_1:4 ;
hence p in LSeg (p1,q) by RLTOPSP1:68; :: thesis: verum
end;
end;
end;
hence ( q in LSeg (p,p2) & p in LSeg (p1,q) ) by A10; :: thesis: verum