for V being RealLinearSpace
for p1, p2 being Point of V holds halfline (p1,p2) c= Line (p1,p2)