for V being RealLinearSpace
for p, q being Element of V
for x being set holds
( x in halfline (p,q) iff ex l being Real st
( x = ((1 - l) * p) + (l * q) & 0 <= l ) ) ;