let f be 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}
let p, q be Point of (TOP-REAL 2); ( p in L~ f & not q in L~ f & <*q*> is_in_the_area_of f implies (LSeg (p,q)) /\ (L~ f) = {p} )
assume that
A1:
p in L~ f
and
A2:
not q in L~ f
and
A3:
<*q*> is_in_the_area_of f
; (LSeg (p,q)) /\ (L~ f) = {p}
A4:
<*p,q*> = <*p*> ^ <*q*>
by FINSEQ_1:def 9;
<*p*> is_in_the_area_of f
by A1, Th46, SPRECT_2:21;
hence
(LSeg (p,q)) /\ (L~ f) c= {p}
by A2, A3, A4, Th47, SPRECT_2:24; XBOOLE_0:def 10 {p} c= (LSeg (p,q)) /\ (L~ f)
p in LSeg (p,q)
by RLTOPSP1:68;
then
p in (LSeg (p,q)) /\ (L~ f)
by A1, XBOOLE_0:def 4;
hence
{p} c= (LSeg (p,q)) /\ (L~ f)
by ZFMISC_1:31; verum