let p, p1, p3, p4 be Point of (TOP-REAL 2); :: thesis: ( p in LSeg p1,p3 & p in LSeg p1,p4 & p3 <> p4 & p <> p1 & not p3 in LSeg p1,p4 implies p4 in LSeg p1,p3 )
assume p in LSeg p1,p3 ; :: thesis: ( not p in LSeg p1,p4 or not p3 <> p4 or not p <> p1 or p3 in LSeg p1,p4 or p4 in LSeg p1,p3 )
then p in { (((1 - l1) * p1) + (l1 * p3)) where l1 is Real : ( 0 <= l1 & l1 <= 1 ) } by TOPREAL1:def 3;
then consider l1 being Real such that
A1: ( p = ((1 - l1) * p1) + (l1 * p3) & 0 <= l1 & l1 <= 1 ) ;
assume p in LSeg p1,p4 ; :: thesis: ( not p3 <> p4 or not p <> p1 or p3 in LSeg p1,p4 or p4 in LSeg p1,p3 )
then p in { (((1 - l2) * p1) + (l2 * p4)) where l2 is Real : ( 0 <= l2 & l2 <= 1 ) } by TOPREAL1:def 3;
then consider l2 being Real such that
A2: ( p = ((1 - l2) * p1) + (l2 * p4) & 0 <= l2 & l2 <= 1 ) ;
assume A3: ( p3 <> p4 & p <> p1 ) ; :: thesis: ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 )
((1 + (- l1)) * p1) + (l1 * p3) = ((1 + (- l2)) * p1) + (l2 * p4) by A1, A2;
then ((1 * p1) + ((- l1) * p1)) + (l1 * p3) = ((1 + (- l2)) * p1) + (l2 * p4) by EUCLID:37;
then ((1 * p1) + ((- l1) * p1)) + (l1 * p3) = ((1 * p1) + ((- l2) * p1)) + (l2 * p4) by EUCLID:37;
then (p1 + ((- l1) * p1)) + (l1 * p3) = ((1 * p1) + ((- l2) * p1)) + (l2 * p4) by EUCLID:33;
then (p1 + ((- l1) * p1)) + (l1 * p3) = (p1 + ((- l2) * p1)) + (l2 * p4) by EUCLID:33;
then (- p1) + (p1 + (((- l1) * p1) + (l1 * p3))) = (- p1) + ((p1 + ((- l2) * p1)) + (l2 * p4)) by EUCLID:30;
then ((- p1) + p1) + (((- l1) * p1) + (l1 * p3)) = (- p1) + ((p1 + ((- l2) * p1)) + (l2 * p4)) by EUCLID:30;
then (0.REAL 2) + (((- l1) * p1) + (l1 * p3)) = (- p1) + ((p1 + ((- l2) * p1)) + (l2 * p4)) by EUCLID:40;
then ((- l1) * p1) + (l1 * p3) = (- p1) + ((p1 + ((- l2) * p1)) + (l2 * p4)) by EUCLID:31;
then ((- l1) * p1) + (l1 * p3) = (- p1) + (p1 + (((- l2) * p1) + (l2 * p4))) by EUCLID:30;
then ((- l1) * p1) + (l1 * p3) = ((- p1) + p1) + (((- l2) * p1) + (l2 * p4)) by EUCLID:30;
then ((- l1) * p1) + (l1 * p3) = (0.REAL 2) + (((- l2) * p1) + (l2 * p4)) by EUCLID:40;
then A4: ((- l1) * p1) + (l1 * p3) = ((- l2) * p1) + (l2 * p4) by EUCLID:31;

per cases ( l1 <= l2 or l1 > l2 ) ;

suppose A5: l1 <= l2 ; :: thesis: ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 )

per cases ( l1 < l2 or l1 = l2 ) by A5, XXREAL_0:1;

suppose A6: l1 < l2 ; :: thesis: ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 )

then l1 / l2 < l2 / l2 by A1, XREAL_1:76;
then A7: l1 / l2 < 1 by A1, A6, XCMPLX_1:60;
((1 / l2) * ((- l1) * p1)) + ((1 / l2) * (l1 * p3)) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by A4, EUCLID:36;
then (((1 / l2) * (- l1)) * p1) + ((1 / l2) * (l1 * p3)) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by EUCLID:34;
then (((- 1) * ((1 / l2) * l1)) * p1) + (((1 / l2) * l1) * p3) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by EUCLID:34;
then (((- 1) * ((l1 / l2) * 1)) * p1) + (((1 / l2) * l1) * p3) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by XCMPLX_1:76;
then ((- (l1 / l2)) * p1) + (((l1 / l2) * 1) * p3) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by XCMPLX_1:76;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = ((1 / l2) * ((- l2) * p1)) + ((1 / l2) * (l2 * p4)) by EUCLID:36;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((1 / l2) * (- l2)) * p1) + ((1 / l2) * (l2 * p4)) by EUCLID:34;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((- 1) * ((1 / l2) * l2)) * p1) + (((1 / l2) * l2) * p4) by EUCLID:34;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((- 1) * ((l2 / l2) * 1)) * p1) + (((1 / l2) * l2) * p4) by XCMPLX_1:76;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((- 1) * (l2 / l2)) * p1) + (((l2 / l2) * 1) * p4) by XCMPLX_1:76;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((- 1) * 1) * p1) + ((l2 / l2) * p4) by A1, A6, XCMPLX_1:60;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = ((- 1) * p1) + (1 * p4) by A1, A6, XCMPLX_1:60;
then A8: ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = p4 + (- p1) by EUCLID:33;
A9: p4 = (p4 - p1) + p1 by EUCLID:52
.= (p1 + ((- (l1 / l2)) * p1)) + ((l1 / l2) * p3) by A8, EUCLID:30
.= ((1 * p1) + ((- (l1 / l2)) * p1)) + ((l1 / l2) * p3) by EUCLID:33
.= ((1 + (- (l1 / l2))) * p1) + ((l1 / l2) * p3) by EUCLID:37
.= ((1 - (l1 / l2)) * p1) + ((l1 / l2) * p3) ;
0 / l2 <= l1 / l2 by A1, A2;
hence ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 ) by A7, A9, SPPOL_1:22; :: thesis: verum

end;

suppose l1 = l2 ; :: thesis: ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 )

then ((l1 * p1) + ((- l1) * p1)) + (l1 * p3) = (l1 * p1) + (((- l1) * p1) + (l1 * p4)) by A4, EUCLID:30;
then ((l1 + (- l1)) * p1) + (l1 * p3) = (l1 * p1) + (((- l1) * p1) + (l1 * p4)) by EUCLID:37;
then (0.REAL 2) + (l1 * p3) = (l1 * p1) + (((- l1) * p1) + (l1 * p4)) by EUCLID:33;
then l1 * p3 = (l1 * p1) + (((- l1) * p1) + (l1 * p4)) by EUCLID:31;
then l1 * p3 = ((l1 * p1) + ((- l1) * p1)) + (l1 * p4) by EUCLID:30;
then l1 * p3 = ((l1 + (- l1)) * p1) + (l1 * p4) by EUCLID:37;
then l1 * p3 = (0.REAL 2) + (l1 * p4) by EUCLID:33;
then A10: l1 * p3 = l1 * p4 by EUCLID:31;

per cases ( l1 = 0 or p3 = p4 ) by A10, EUCLID:38;

suppose l1 = 0 ; :: thesis: ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 )

then p = p1 + (0 * p3) by A1, EUCLID:33
.= p1 + (0.REAL 2) by EUCLID:33
.= p1 by EUCLID:31 ;
hence ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 ) by A3; :: thesis: verum

end;

suppose p3 = p4 ; :: thesis: ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 )

hence ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 ) by A3; :: thesis: verum

end;

end;

end;

end;

end;

suppose A11: l1 > l2 ; :: thesis: ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 )

then l2 / l1 < l1 / l1 by A2, XREAL_1:76;
then A12: l2 / l1 < 1 by A2, A11, XCMPLX_1:60;
((1 / l1) * ((- l1) * p1)) + ((1 / l1) * (l1 * p3)) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by A4, EUCLID:36;
then (((1 / l1) * (- l1)) * p1) + ((1 / l1) * (l1 * p3)) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by EUCLID:34;
then (((- 1) * ((1 / l1) * l1)) * p1) + (((1 / l1) * l1) * p3) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by EUCLID:34;
then (((- 1) * ((l1 / l1) * 1)) * p1) + (((1 / l1) * l1) * p3) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by XCMPLX_1:76;
then ((- (l1 / l1)) * p1) + (((l1 / l1) * 1) * p3) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by XCMPLX_1:76;
then ((- 1) * p1) + (((l1 / l1) * 1) * p3) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by A2, A11, XCMPLX_1:60;
then (1 * p3) + ((- 1) * p1) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by A2, A11, XCMPLX_1:60;
then p3 + (- p1) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by EUCLID:33;
then p3 - p1 = ((1 / l1) * ((- l2) * p1)) + ((1 / l1) * (l2 * p4)) by EUCLID:36;
then p3 - p1 = (((1 / l1) * (- l2)) * p1) + ((1 / l1) * (l2 * p4)) by EUCLID:34;
then p3 - p1 = (((- 1) * ((1 / l1) * l2)) * p1) + (((1 / l1) * l2) * p4) by EUCLID:34;
then A13: p3 - p1 = (((- 1) * ((l2 / l1) * 1)) * p1) + (((1 / l1) * l2) * p4) by XCMPLX_1:76;
A14: p3 = (p3 - p1) + p1 by EUCLID:52
.= (((- (l2 / l1)) * p1) + ((l2 / l1) * p4)) + p1 by A13, XCMPLX_1:76
.= (p1 + ((- (l2 / l1)) * p1)) + ((l2 / l1) * p4) by EUCLID:30
.= ((1 * p1) + ((- (l2 / l1)) * p1)) + ((l2 / l1) * p4) by EUCLID:33
.= ((1 + (- (l2 / l1))) * p1) + ((l2 / l1) * p4) by EUCLID:37
.= ((1 - (l2 / l1)) * p1) + ((l2 / l1) * p4) ;
0 / l1 <= l2 / l1 by A1, A2;
hence ( p3 in LSeg p1,p4 or p4 in LSeg p1,p3 ) by A12, A14, SPPOL_1:22; :: thesis: verum

end;

end;