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, Th46, SPRECT_2:21;
hence (LSeg (p,q)) /\ (L~ f) c= {p} by A2, A3, A4, Th47, SPRECT_2:24; :: according to XBOOLE_0:def 10 :: thesis: {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; :: thesis: verum