let p1, p3, p4, p 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 consider l1 being Real such that
A1: p = ((1 - l1) * p1) + (l1 * p3) and
A2: 0 <= l1 and
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 consider l2 being Real such that
A3: p = ((1 - l2) * p1) + (l2 * p4) and
A4: 0 <= l2 and
l2 <= 1 ;
((1 + (- l1)) * p1) + (l1 * p3) = ((1 + (- l2)) * p1) + (l2 * p4) by A1, A3;
then ((1 * p1) + ((- l1) * p1)) + (l1 * p3) = ((1 + (- l2)) * p1) + (l2 * p4) by RLVECT_1:def 6;
then ((1 * p1) + ((- l1) * p1)) + (l1 * p3) = ((1 * p1) + ((- l2) * p1)) + (l2 * p4) by RLVECT_1:def 6;
then (p1 + ((- l1) * p1)) + (l1 * p3) = ((1 * p1) + ((- l2) * p1)) + (l2 * p4) by RLVECT_1:def 8;
then (p1 + ((- l1) * p1)) + (l1 * p3) = (p1 + ((- l2) * p1)) + (l2 * p4) by RLVECT_1:def 8;
then (- p1) + (p1 + (((- l1) * p1) + (l1 * p3))) = (- p1) + ((p1 + ((- l2) * p1)) + (l2 * p4)) by RLVECT_1:def 3;
then ((- p1) + p1) + (((- l1) * p1) + (l1 * p3)) = (- p1) + ((p1 + ((- l2) * p1)) + (l2 * p4)) by RLVECT_1:def 3;
then (0. (TOP-REAL 2)) + (((- l1) * p1) + (l1 * p3)) = (- p1) + ((p1 + ((- l2) * p1)) + (l2 * p4)) by RLVECT_1:5;
then ((- l1) * p1) + (l1 * p3) = (- p1) + ((p1 + ((- l2) * p1)) + (l2 * p4)) by RLVECT_1:4;
then ((- l1) * p1) + (l1 * p3) = (- p1) + (p1 + (((- l2) * p1) + (l2 * p4))) by RLVECT_1:def 3;
then ((- l1) * p1) + (l1 * p3) = ((- p1) + p1) + (((- l2) * p1) + (l2 * p4)) by RLVECT_1:def 3;
then ((- l1) * p1) + (l1 * p3) = (0. (TOP-REAL 2)) + (((- l2) * p1) + (l2 * p4)) by RLVECT_1:5;
then A5: ((- l1) * p1) + (l1 * p3) = ((- l2) * p1) + (l2 * p4) by RLVECT_1:4;
assume that
A6: p3 <> p4 and
A7: p <> p1 ; :: thesis: ( p3 in LSeg (p1,p4) or p4 in LSeg (p1,p3) )
per cases ( l1 <= l2 or l1 > l2 ) ;
suppose A8: l1 <= l2 ; :: thesis: ( p3 in LSeg (p1,p4) or p4 in LSeg (p1,p3) )
per cases ( l1 < l2 or l1 = l2 ) by A8, XXREAL_0:1;
suppose A9: l1 < l2 ; :: thesis: ( p3 in LSeg (p1,p4) or p4 in LSeg (p1,p3) )
((1 / l2) * ((- l1) * p1)) + ((1 / l2) * (l1 * p3)) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by A5, RLVECT_1:def 5;
then (((1 / l2) * (- l1)) * p1) + ((1 / l2) * (l1 * p3)) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by RLVECT_1:def 7;
then (((- 1) * ((1 / l2) * l1)) * p1) + (((1 / l2) * l1) * p3) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by RLVECT_1:def 7;
then (((- 1) * ((l1 / l2) * 1)) * p1) + (((1 / l2) * l1) * p3) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by XCMPLX_1:75;
then ((- (l1 / l2)) * p1) + (((l1 / l2) * 1) * p3) = (1 / l2) * (((- l2) * p1) + (l2 * p4)) by XCMPLX_1:75;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = ((1 / l2) * ((- l2) * p1)) + ((1 / l2) * (l2 * p4)) by RLVECT_1:def 5;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((1 / l2) * (- l2)) * p1) + ((1 / l2) * (l2 * p4)) by RLVECT_1:def 7;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((- 1) * ((1 / l2) * l2)) * p1) + (((1 / l2) * l2) * p4) by RLVECT_1:def 7;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((- 1) * ((l2 / l2) * 1)) * p1) + (((1 / l2) * l2) * p4) by XCMPLX_1:75;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((- 1) * (l2 / l2)) * p1) + (((l2 / l2) * 1) * p4) by XCMPLX_1:75;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (((- 1) * 1) * p1) + ((l2 / l2) * p4) by A2, A9, XCMPLX_1:60;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = ((- 1) * p1) + (1 * p4) by A2, A9, XCMPLX_1:60;
then ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = (- p1) + (1 * p4) ;
then A10: ((- (l1 / l2)) * p1) + ((l1 / l2) * p3) = p4 + (- p1) by RLVECT_1:def 8;
l1 / l2 < l2 / l2 by A2, A9, XREAL_1:74;
then A11: l1 / l2 < 1 by A2, A9, XCMPLX_1:60;
p4 = (p4 - p1) + p1 by RLVECT_4:1
.= (p1 + ((- (l1 / l2)) * p1)) + ((l1 / l2) * p3) by A10, RLVECT_1:def 3
.= ((1 * p1) + ((- (l1 / l2)) * p1)) + ((l1 / l2) * p3) by RLVECT_1:def 8
.= ((1 + (- (l1 / l2))) * p1) + ((l1 / l2) * p3) by RLVECT_1:def 6
.= ((1 - (l1 / l2)) * p1) + ((l1 / l2) * p3) ;
hence ( p3 in LSeg (p1,p4) or p4 in LSeg (p1,p3) ) by A2, A4, A11; :: 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 A5, RLVECT_1:def 3;
then ((l1 + (- l1)) * p1) + (l1 * p3) = (l1 * p1) + (((- l1) * p1) + (l1 * p4)) by RLVECT_1:def 6;
then (0. (TOP-REAL 2)) + (l1 * p3) = (l1 * p1) + (((- l1) * p1) + (l1 * p4)) by RLVECT_1:10;
then l1 * p3 = (l1 * p1) + (((- l1) * p1) + (l1 * p4)) by RLVECT_1:4;
then l1 * p3 = ((l1 * p1) + ((- l1) * p1)) + (l1 * p4) by RLVECT_1:def 3;
then l1 * p3 = ((l1 + (- l1)) * p1) + (l1 * p4) by RLVECT_1:def 6;
then l1 * p3 = (0. (TOP-REAL 2)) + (l1 * p4) by RLVECT_1:10;
then A12: l1 * p3 = l1 * p4 by RLVECT_1:4;
per cases ( l1 = 0 or p3 = p4 ) by A12, RLVECT_1:36;
suppose l1 = 0 ; :: thesis: ( p3 in LSeg (p1,p4) or p4 in LSeg (p1,p3) )
then p = p1 + (0 * p3) by A1, RLVECT_1:def 8
.= p1 + (0. (TOP-REAL 2)) by RLVECT_1:10
.= p1 by RLVECT_1:4 ;
hence ( p3 in LSeg (p1,p4) or p4 in LSeg (p1,p3) ) by A7; :: 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 A6; :: thesis: verum
end;
end;
end;
end;
end;
suppose A13: l1 > l2 ; :: thesis: ( p3 in LSeg (p1,p4) or p4 in LSeg (p1,p3) )
((1 / l1) * ((- l1) * p1)) + ((1 / l1) * (l1 * p3)) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by A5, RLVECT_1:def 5;
then (((1 / l1) * (- l1)) * p1) + ((1 / l1) * (l1 * p3)) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by RLVECT_1:def 7;
then (((- 1) * ((1 / l1) * l1)) * p1) + (((1 / l1) * l1) * p3) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by RLVECT_1:def 7;
then (((- 1) * ((l1 / l1) * 1)) * p1) + (((1 / l1) * l1) * p3) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by XCMPLX_1:75;
then ((- (l1 / l1)) * p1) + (((l1 / l1) * 1) * p3) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by XCMPLX_1:75;
then ((- 1) * p1) + (((l1 / l1) * 1) * p3) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by A4, A13, XCMPLX_1:60;
then (1 * p3) + ((- 1) * p1) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by A4, A13, XCMPLX_1:60;
then (1 * p3) + (- p1) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) ;
then p3 + (- p1) = (1 / l1) * (((- l2) * p1) + (l2 * p4)) by RLVECT_1:def 8;
then p3 - p1 = ((1 / l1) * ((- l2) * p1)) + ((1 / l1) * (l2 * p4)) by RLVECT_1:def 5;
then p3 - p1 = (((1 / l1) * (- l2)) * p1) + ((1 / l1) * (l2 * p4)) by RLVECT_1:def 7;
then p3 - p1 = (((- 1) * ((1 / l1) * l2)) * p1) + (((1 / l1) * l2) * p4) by RLVECT_1:def 7;
then A14: p3 - p1 = (((- 1) * ((l2 / l1) * 1)) * p1) + (((1 / l1) * l2) * p4) by XCMPLX_1:75;
l2 / l1 < l1 / l1 by A4, A13, XREAL_1:74;
then A15: l2 / l1 < 1 by A4, A13, XCMPLX_1:60;
p3 = (p3 - p1) + p1 by RLVECT_4:1
.= (((- (l2 / l1)) * p1) + ((l2 / l1) * p4)) + p1 by A14, XCMPLX_1:75
.= (p1 + ((- (l2 / l1)) * p1)) + ((l2 / l1) * p4) by RLVECT_1:def 3
.= ((1 * p1) + ((- (l2 / l1)) * p1)) + ((l2 / l1) * p4) by RLVECT_1:def 8
.= ((1 + (- (l2 / l1))) * p1) + ((l2 / l1) * p4) by RLVECT_1:def 6
.= ((1 - (l2 / l1)) * p1) + ((l2 / l1) * p4) ;
hence ( p3 in LSeg (p1,p4) or p4 in LSeg (p1,p3) ) by A2, A4, A15; :: thesis: verum
end;
end;