let V be RealLinearSpace; :: thesis: for p1, p2, p3 being Point of V holds
( p1,p2,p3 are_collinear iff ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) ) )
let p1, p2, p3 be Point of V; :: thesis: ( p1,p2,p3 are_collinear iff ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) ) )
thus ( not p1,p2,p3 are_collinear or p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) ) :: thesis: ( ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) ) implies p1,p2,p3 are_collinear )

proof

assume p1,p2,p3 are_collinear ; :: thesis: ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) )
then consider L being line of V such that
A1: p1 in L and
A2: p2 in L and
A3: p3 in L ;
consider x1, x2 being Point of V such that
A4: L = Line (x1,x2) by RLTOPSP1:def 15;

per cases ( p2 = p3 or p2 <> p3 ) ;

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

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

end;

suppose p2 <> p3 ; :: thesis: ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) )

then A5: Line (p2,p3) = L by A2, A3, RLTOPSP1:75, A4;

per cases ( p1 in halfline (p2,p3) or not p1 in halfline (p2,p3) ) ;

suppose p1 in halfline (p2,p3) ; :: thesis: ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) )

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

end;

suppose A6: not p1 in halfline (p2,p3) ; :: thesis: ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) )

L = (halfline (p2,p3)) \/ (halfline (p3,p2)) by Th63, A5;
then p1 in halfline (p3,p2) by A1, XBOOLE_0:def 3, A6;
hence ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) ) by Th64; :: thesis: verum

end;

end;

end;

end;

end;

assume ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) ) ; :: thesis: p1,p2,p3 are_collinear

per cases then ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) ) ;

suppose A7: p1 in LSeg (p2,p3) ; :: thesis: p1,p2,p3 are_collinear

take Line (p2,p3) ; :: according to RLTOPSP1:def 16 :: thesis: ( p1 in Line (p2,p3) & p2 in Line (p2,p3) & p3 in Line (p2,p3) )
LSeg (p2,p3) c= Line (p2,p3) by RLTOPSP1:73;
hence p1 in Line (p2,p3) by A7; :: thesis: ( p2 in Line (p2,p3) & p3 in Line (p2,p3) )
thus p2 in Line (p2,p3) by RLTOPSP1:72; :: thesis: p3 in Line (p2,p3)
thus p3 in Line (p2,p3) by RLTOPSP1:72; :: thesis: verum

end;

suppose A8: p2 in LSeg (p3,p1) ; :: thesis: p1,p2,p3 are_collinear

take Line (p3,p1) ; :: according to RLTOPSP1:def 16 :: thesis: ( p1 in Line (p3,p1) & p2 in Line (p3,p1) & p3 in Line (p3,p1) )
thus p1 in Line (p3,p1) by RLTOPSP1:72; :: thesis: ( p2 in Line (p3,p1) & p3 in Line (p3,p1) )
LSeg (p3,p1) c= Line (p3,p1) by RLTOPSP1:73;
hence p2 in Line (p3,p1) by A8; :: thesis: p3 in Line (p3,p1)
thus p3 in Line (p3,p1) by RLTOPSP1:72; :: thesis: verum

end;

suppose A9: p3 in LSeg (p1,p2) ; :: thesis: p1,p2,p3 are_collinear

take Line (p1,p2) ; :: according to RLTOPSP1:def 16 :: thesis: ( p1 in Line (p1,p2) & p2 in Line (p1,p2) & p3 in Line (p1,p2) )
thus p1 in Line (p1,p2) by RLTOPSP1:72; :: thesis: ( p2 in Line (p1,p2) & p3 in Line (p1,p2) )
thus p2 in Line (p1,p2) by RLTOPSP1:72; :: thesis: p3 in Line (p1,p2)
LSeg (p1,p2) c= Line (p1,p2) by RLTOPSP1:73;
hence p3 in Line (p1,p2) by A9; :: thesis: verum

end;

end;