:: deftheorem defines Line RLTOPSP1:def 14 :
for V being RealLinearSpace
for v, w being Point of V holds Line (v,w) = { (((1 - r) * v) + (r * w)) where r is Real : verum } ;