:: deftheorem defines halfline TOPREAL9:def 5 :
for V being RealLinearSpace
for p, q being Element of V holds halfline (p,q) = { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ;