let f be rectangular FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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 ; :: thesis: (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, Th63, SPRECT_2:25;
hence (LSeg p,q) /\ (L~ f) c= {p} by A2, A3, A4, Th64, SPRECT_2:28; :: according to XBOOLE_0:def 10 :: thesis: {p} c= (LSeg p,q) /\ (L~ f)
p in LSeg p,q by RLTOPSP1:69;
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:37; :: thesis: verum