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