theorem :: TOPREAL9:67

for V being RealLinearSpace
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) ) )