for V being RealLinearSpace
for p, q, x being Element of V st x in halfline (p,q) holds
halfline (p,x) c= halfline (p,q)