let V be RealLinearSpace; :: thesis: for p1, p2, p3 being Point of V holds
( not p1 in halfline (p2,p3) or p1 in LSeg (p2,p3) or p3 in LSeg (p2,p1) )
let p1, p2, p3 be Point of V; :: thesis: ( not p1 in halfline (p2,p3) or p1 in LSeg (p2,p3) or p3 in LSeg (p2,p1) )
assume p1 in halfline (p2,p3) ; :: thesis: ( p1 in LSeg (p2,p3) or p3 in LSeg (p2,p1) )
then consider r being Real such that
A1: p1 = ((1 - r) * p2) + (r * p3) and
A2: 0 <= r ;
set s = 1 / r;

now :: thesis: ( ( r <= 1 & p1 in LSeg (p2,p3) ) or ( r >= 1 & ( ( r = 0 & p1 in LSeg (p2,p3) ) or ( r > 0 & p3 in LSeg (p2,p1) ) ) ) )

per cases ( r <= 1 or r >= 1 ) ;

case r <= 1 ; :: thesis: p1 in LSeg (p2,p3)

hence p1 in LSeg (p2,p3) by A1, A2; :: thesis: verum

end;

case A3: r >= 1 ; :: thesis: verum

per cases ( r = 0 or r > 0 ) by A2;

case r = 0 ; :: thesis: p1 in LSeg (p2,p3)

then p1 = p2 by A1, Th2;
hence p1 in LSeg (p2,p3) by RLTOPSP1:68; :: thesis: verum

end;

case A4: r > 0 ; :: thesis: p3 in LSeg (p2,p1)

then A5: (1 / r) * r = 1 by XCMPLX_1:87;
A6: 1 / r <= 1 by A3, XREAL_1:183;
A7: r * p3 = p1 - ((1 - r) * p2) by RLVECT_4:1, A1;
((1 / r) * r) * p3 = (1 / r) * (r * p3) by RLVECT_1:def 7
.= ((1 / r) * p1) - ((1 / r) * ((1 - r) * p2)) by RLVECT_1:34, A7
.= ((1 / r) * p1) - (((1 / r) * (1 - r)) * p2) by RLVECT_1:def 7 ;
then p3 = ((1 / r) * p1) - (((1 / r) * (1 - r)) * p2) by RLVECT_1:def 8, A5
.= ((1 / r) * p1) + ((- ((1 / r) * (1 - r))) * p2) by RLVECT_1:79
.= ((1 / r) * p1) + ((1 - (1 / r)) * p2) by A5 ;
hence p3 in LSeg (p2,p1) by A4, A6; :: thesis: verum

end;

end;

end;

end;

end;

hence ( p1 in LSeg (p2,p3) or p3 in LSeg (p2,p1) ) ; :: thesis: verum