let f be S-Sequence_in_R2; for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. (len f) in Q holds
(L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
let Q be closed Subset of (TOP-REAL 2); ( L~ f meets Q & not f /. (len f) in Q implies (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} )
assume that
A1:
L~ f meets Q
and
A2:
not f /. (len f) in Q
; (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
set p1 = f /. 1;
set p2 = f /. (len f);
set lp = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q);
A3:
(L~ f) /\ Q is closed
by TOPS_1:8;
len f >= 1 + 1
by TOPREAL1:def 8;
then A4:
len f > 1
by NAT_1:13;
then AA:
len f in dom f
by FINSEQ_3:25;
L~ f is_an_arc_of f /. 1,f /. (len f)
by TOPREAL1:25;
then A5:
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q
by A1, A3, JORDAN5C:def 2;
then A6:
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ f
by XBOOLE_0:def 4;
then A7:
1 <= Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)
by JORDAN3:8;
A8:
now (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q c= {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}set m =
mid (
f,
((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),
(len f));
assume
not
(L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q c= {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
;
contradictionthen consider q being
object such that A9:
q in (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q
and A10:
not
q in {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
by TARSKI:def 3;
reconsider q =
q as
Point of
(TOP-REAL 2) by A9;
A11:
q in L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))
by A9, XBOOLE_0:def 4;
A12:
L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) c= L~ f
by A6, JORDAN3:42;
A13:
Index (
(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),
f)
< len f
by A6, JORDAN3:8;
then A14:
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1
<= len f
by NAT_1:13;
A15:
1
<= (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1
by NAT_1:11;
then
len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = ((len f) -' ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)) + 1
by A14, JORDAN4:8;
then A16:
not
mid (
f,
((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),
(len f)) is
empty
by CARD_1:27;
A17:
q <> Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
by A10, TARSKI:def 1;
q in Q
by A9, XBOOLE_0:def 4;
then A18:
LE q,
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q),
L~ f,
f /. 1,
f /. (len f)
by A3, A11, A12, JORDAN5C:16;
per cases
( Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) or Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) )
;
suppose
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
= f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)
;
contradictionthen A19:
q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))
by A11, JORDAN3:def 3;
now not (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len fassume
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1
>= len f
;
contradictionthen
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1
= len f
by A14, XXREAL_0:1;
then
len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1
by AA, JORDAN4:15;
hence
contradiction
by A19, TOPREAL1:22;
verum end; then A20:
LE f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),
q,
L~ f,
f /. 1,
f /. (len f)
by A19, Th3, NAT_1:11;
A21:
f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) in LSeg (
(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),
(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)))
by RLTOPSP1:68;
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
in LSeg (
f,
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))
by A6, JORDAN3:9;
then
LE Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q),
f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),
L~ f,
f /. 1,
f /. (len f)
by A7, A13, A21, Th4;
then
LE Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q),
q,
L~ f,
f /. 1,
f /. (len f)
by A20, JORDAN5C:13;
hence
contradiction
by A17, A18, JORDAN5C:12, TOPREAL1:25;
verum end; suppose A22:
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
<> f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)
;
contradictionA23:
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
in LSeg (
f,
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))
by A6, JORDAN3:9;
1
<= (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1
by NAT_1:11;
then A24:
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1
in dom f
by A14, FINSEQ_3:25;
q in L~ (<*(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> ^ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))))
by A11, A22, JORDAN3:def 3;
then A25:
q in (L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))) \/ (LSeg (((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1),(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))
by A16, SPPOL_2:20;
now contradictionper cases
( q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) or q in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1)) )
by A25, XBOOLE_0:def 3;
suppose A26:
q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))
;
contradictionnow not (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len fassume
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1
>= len f
;
contradictionthen
(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1
= len f
by A14, XXREAL_0:1;
then
len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1
by AA, JORDAN4:15;
hence
contradiction
by A26, TOPREAL1:22;
verum end; then A27:
LE f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),
q,
L~ f,
f /. 1,
f /. (len f)
by A26, Th3, NAT_1:11;
f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) in LSeg (
(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),
(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)))
by RLTOPSP1:68;
then
LE Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q),
f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),
L~ f,
f /. 1,
f /. (len f)
by A7, A13, A23, Th4;
then
LE Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q),
q,
L~ f,
f /. 1,
f /. (len f)
by A27, JORDAN5C:13;
hence
contradiction
by A17, A18, JORDAN5C:12, TOPREAL1:25;
verum end; suppose A28:
q in LSeg (
(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),
((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1))
;
contradiction
1
in dom (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))
by A16, FINSEQ_5:6;
then (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1 =
(mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) . 1
by PARTFUN1:def 6
.=
f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)
by A4, A14, A15, FINSEQ_6:118
.=
f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)
by A24, PARTFUN1:def 6
;
then
LE Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q),
q,
L~ f,
f /. 1,
f /. (len f)
by A7, A13, A23, A28, Th4;
hence
contradiction
by A17, A18, JORDAN5C:12, TOPREAL1:25;
verum end; end; end; hence
contradiction
;
verum end; end; end;
A29:
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in Q
by A5, XBOOLE_0:def 4;
len f in dom f
by A4, FINSEQ_3:25;
then
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . (len f)
by A2, A29, PARTFUN1:def 6;
then
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))
by A6, JORDAN5B:19;
then
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q
by A29, XBOOLE_0:def 4;
hence
(L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
by A8, ZFMISC_1:33; verum