theorem Th47: :: SPRECT_3:47

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