theorem Th25: :: TOPREAL9:27

for V being RealLinearSpace
for p, q being Element of V holds p in halfline (p,q)