theorem LMOPN: :: NDIFF_5:16
for S being RealLinearSpace
for p, q being Point of S st p <> q holds
].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) }