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}
then
<*q*> is_in_the_area_of f
by Th59;
then A3:
( q `1 <> W-bound (L~ f) & q `1 <> E-bound (L~ f) & q `2 <> S-bound (L~ f) & q `2 <> N-bound (L~ f) )
by A1, Th60;
A4:
dom <*p,q*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
then A5:
1 in dom <*p,q*>
by TARSKI:def 2;
A6:
<*p,q*> /. 1 = p
by FINSEQ_4:26;
then A7:
( W-bound (L~ f) <= p `1 & p `1 <= E-bound (L~ f) )
by A2, A5, SPRECT_2:def 1;
A8:
( S-bound (L~ f) <= p `2 & p `2 <= N-bound (L~ f) )
by A2, A5, A6, SPRECT_2:def 1;
A9:
2 in dom <*p,q*>
by A4, TARSKI:def 2;
A10:
<*p,q*> /. 2 = q
by FINSEQ_4:26;
then
( W-bound (L~ f) <= q `1 & q `1 <= E-bound (L~ f) )
by A2, A9, SPRECT_2:def 1;
then A11:
( W-bound (L~ f) < q `1 & q `1 < E-bound (L~ f) )
by A3, XXREAL_0:1;
( S-bound (L~ f) <= q `2 & q `2 <= N-bound (L~ f) )
by A2, A9, A10, SPRECT_2:def 1;
then A12:
( S-bound (L~ f) < q `2 & q `2 < N-bound (L~ f) )
by A3, XXREAL_0:1;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg p,q) /\ (L~ f) or x in {p} )
assume A13:
x in (LSeg p,q) /\ (L~ f)
; :: thesis: x in {p}
then A14:
x in LSeg p,q
by XBOOLE_0:def 4;
reconsider p' = x as Point of (TOP-REAL 2) by A13;
consider r being Real such that
A17:
p' = ((1 - r) * p) + (r * q)
and
A15:
0 <= r
and
A16:
r <= 1
by A14;
A18: p' `1 =
(((1 - r) * p) `1 ) + ((r * q) `1 )
by A17, TOPREAL3:7
.=
((1 - r) * (p `1 )) + ((r * q) `1 )
by TOPREAL3:9
.=
((1 - r) * (p `1 )) + (r * (q `1 ))
by TOPREAL3:9
;
A19: p' `2 =
(((1 - r) * p) `2 ) + ((r * q) `2 )
by A17, TOPREAL3:7
.=
((1 - r) * (p `2 )) + ((r * q) `2 )
by TOPREAL3:9
.=
((1 - r) * (p `2 )) + (r * (q `2 ))
by TOPREAL3:9
;
A20:
p' in L~ f
by A13, XBOOLE_0:def 4;