let f be 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}
let p, q be Point of (TOP-REAL 2); ( 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
; ( 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
; (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 ; TARSKI:def 3 ( 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)
; 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
;