theorem :: SPRECT_3:48

for f being rectangular FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f holds
(LSeg (p,q)) /\ (L~ f) = {p}