let f be rectangular FinSequence of (TOP-REAL 2); :: thesis: 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}
let p, q be Point of (TOP-REAL 2); :: thesis: ( not q in L~ f & <*p,q*> is_in_the_area_of f implies (LSeg (p,q)) /\ (L~ f) c= {p} )
assume A1: not q in L~ f ; :: thesis: ( not <*p,q*> is_in_the_area_of f or (LSeg (p,q)) /\ (L~ f) c= {p} )
assume A2: <*p,q*> is_in_the_area_of f ; :: thesis: (LSeg (p,q)) /\ (L~ f) c= {p}
A3: dom <*p,q*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then A4: 2 in dom <*p,q*> by TARSKI:def 2;
A5: <*p,q*> /. 2 = q by FINSEQ_4:17;
then A6: W-bound (L~ f) <= q `1 by A2, A4;
A7: <*q*> is_in_the_area_of f by A2, Th42;
then q `1 <> W-bound (L~ f) by A1, Th43;
then A8: W-bound (L~ f) < q `1 by A6, XXREAL_0:1;
A9: q `2 <= N-bound (L~ f) by A2, A4, A5;
q `2 <> N-bound (L~ f) by A1, A7, Th43;
then A10: q `2 < N-bound (L~ f) by A9, XXREAL_0:1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (p,q)) /\ (L~ f) or x in {p} )
A11: <*p,q*> /. 1 = p by FINSEQ_4:17;
A12: q `1 <= E-bound (L~ f) by A2, A4, A5;
q `1 <> E-bound (L~ f) by A1, A7, Th43;
then A13: q `1 < E-bound (L~ f) by A12, XXREAL_0:1;
assume A14: x in (LSeg (p,q)) /\ (L~ f) ; :: thesis: x in {p}
then reconsider p9 = x as Point of (TOP-REAL 2) ;
A15: p9 in L~ f by A14, XBOOLE_0:def 4;
A16: 1 in dom <*p,q*> by A3, TARSKI:def 2;
then A17: W-bound (L~ f) <= p `1 by A2, A11;
A18: p `2 <= N-bound (L~ f) by A2, A16, A11;
A19: S-bound (L~ f) <= p `2 by A2, A16, A11;
A20: p `1 <= E-bound (L~ f) by A2, A16, A11;
A21: S-bound (L~ f) <= q `2 by A2, A4, A5;
q `2 <> S-bound (L~ f) by A1, A7, Th43;
then A22: S-bound (L~ f) < q `2 by A21, XXREAL_0:1;
x in LSeg (p,q) by A14, XBOOLE_0:def 4;
then consider r being Real such that
A23: p9 = ((1 - r) * p) + (r * q) and
A24: 0 <= r and
A25: r <= 1 ;
A26: p9 `1 = (((1 - r) * p) `1) + ((r * q) `1) by A23, TOPREAL3:2
.= ((1 - r) * (p `1)) + ((r * q) `1) by TOPREAL3:4
.= ((1 - r) * (p `1)) + (r * (q `1)) by TOPREAL3:4 ;
A27: p9 `2 = (((1 - r) * p) `2) + ((r * q) `2) by A23, TOPREAL3:2
.= ((1 - r) * (p `2)) + ((r * q) `2) by TOPREAL3:4
.= ((1 - r) * (p `2)) + (r * (q `2)) by TOPREAL3:4 ;

per cases ( p9 `1 = W-bound (L~ f) or p9 `1 = E-bound (L~ f) or p9 `2 = S-bound (L~ f) or p9 `2 = N-bound (L~ f) ) by A15, Th32;

suppose p9 `1 = W-bound (L~ f) ; :: thesis: x in {p}

then r = 0 by A17, A8, A24, A25, A26, XREAL_1:180;
then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, RLVECT_1:10
.= 1 * p by RLVECT_1:4
.= p by RLVECT_1:def 8 ;
hence x in {p} by ZFMISC_1:31; :: thesis: verum

end;

suppose p9 `1 = E-bound (L~ f) ; :: thesis: x in {p}

then r = 0 by A20, A13, A24, A25, A26, XREAL_1:179;
then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, RLVECT_1:10
.= 1 * p by RLVECT_1:4
.= p by RLVECT_1:def 8 ;
hence x in {p} by ZFMISC_1:31; :: thesis: verum

end;

suppose p9 `2 = S-bound (L~ f) ; :: thesis: x in {p}

then r = 0 by A19, A22, A24, A25, A27, XREAL_1:180;
then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, RLVECT_1:10
.= 1 * p by RLVECT_1:4
.= p by RLVECT_1:def 8 ;
hence x in {p} by ZFMISC_1:31; :: thesis: verum

end;

suppose p9 `2 = N-bound (L~ f) ; :: thesis: x in {p}

then r = 0 by A18, A10, A24, A25, A27, XREAL_1:179;
then p9 = (1 * p) + (0. (TOP-REAL 2)) by A23, RLVECT_1:10
.= 1 * p by RLVECT_1:4
.= p by RLVECT_1:def 8 ;
hence x in {p} by ZFMISC_1:31; :: thesis: verum

end;

end;