assume A1: P is being_simple_closed_curve ; :: thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) & ( for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ) )
then consider f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) such that
A2: f is being_homeomorphism ;
A3: dom f = [#] ((TOP-REAL 2) | R^2-unit_square) by A2;
A4: [#] ((TOP-REAL 2) | P) c= [#] (TOP-REAL 2) by PRE_TOPC:def 4;
A5: f is continuous by A2;
thus ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) by A1, Th4; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
set RS = R^2-unit_square ;
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 <> p2 & p1 in P & p2 in P implies ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) )
assume that
A6: p1 <> p2 and
A7: p1 in P and
A8: p2 in P ; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A9: [#] ((TOP-REAL 2) | R^2-unit_square) = R^2-unit_square by PRE_TOPC:def 5;
set q1 = (f ") . p1;
set q2 = (f ") . p2;
A10: [#] ((TOP-REAL 2) | R^2-unit_square) c= [#] (TOP-REAL 2) by PRE_TOPC:def 4;
A11: I[01] is compact by HEINE:4, TOPMETR:20;
A12: f is one-to-one by A2;
A13: rng f = [#] ((TOP-REAL 2) | P) by A2;
then f is onto by FUNCT_2:def 3;
then A14: f " = f " by A12, TOPS_2:def 4;
then A15: rng (f ") = dom f by A12, FUNCT_1:33;
A16: dom (f ") = rng f by A12, A14, FUNCT_1:32;
then A17: p1 in dom (f ") by A7, A13, PRE_TOPC:def 5;
A18: p2 in dom (f ") by A8, A13, A16, PRE_TOPC:def 5;
reconsider f = f as Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) ;
A19: (f ") . p1 in rng (f ") by A17, FUNCT_1:def 3;
A20: (f ") . p2 in rng (f ") by A18, FUNCT_1:def 3;
reconsider q1 = (f ") . p1, q2 = (f ") . p2 as Point of (TOP-REAL 2) by A10, A19, A20;
A21: q1 <> q2 by A6, A12, A14, A17, A18, FUNCT_1:def 4;
A22: dom f = the carrier of ((TOP-REAL 2) | R^2-unit_square) by FUNCT_2:def 1;
then A23: q2 in R^2-unit_square by A15, A18, A9, FUNCT_1:def 3;
A24: p1 = f . q1 by A12, A14, A16, A17, FUNCT_1:35;
q1 in R^2-unit_square by A15, A17, A22, A9, FUNCT_1:def 3;
then consider Q1, Q2 being non empty Subset of (TOP-REAL 2) such that
A25: Q1 is_an_arc_of q1,q2 and
A26: Q2 is_an_arc_of q1,q2 and
A27: R^2-unit_square = Q1 \/ Q2 and
A28: Q1 /\ Q2 = {q1,q2} by A21, A23, Th1;
A29: Q2 c= dom f by A22, A9, A27, XBOOLE_1:7;
set P1 = f .: Q1;
set P2 = f .: Q2;
Q1 c= dom f by A22, A9, A27, XBOOLE_1:7;
then reconsider P1 = f .: Q1, P2 = f .: Q2 as non empty Subset of (TOP-REAL 2) by A29, A4, XBOOLE_1:1;
A30: rng (f | Q1) = P1 by RELAT_1:115
.= [#] ((TOP-REAL 2) | P1) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2) | P1) ;
dom (f | Q1) = R^2-unit_square /\ Q1 by A22, A9, RELAT_1:61
.= Q1 by A27, XBOOLE_1:21
.= [#] ((TOP-REAL 2) | Q1) by PRE_TOPC:def 5 ;
then reconsider F1 = f | Q1 as Function of ((TOP-REAL 2) | Q1),((TOP-REAL 2) | P1) by A30, FUNCT_2:def 1, RELSET_1:4;
A31: f " P1 c= Q1 by A12, FUNCT_1:82;
[#] ((TOP-REAL 2) | Q1) = Q1 by PRE_TOPC:def 5;
then A32: (TOP-REAL 2) | Q1 is SubSpace of (TOP-REAL 2) | R^2-unit_square by A9, A27, TOPMETR:3, XBOOLE_1:7;
Q1 c= f " P1 by A22, A9, A27, FUNCT_1:76, XBOOLE_1:7;
then A33: f " P1 = Q1 by A31, XBOOLE_0:def 10;
for R being Subset of ((TOP-REAL 2) | P1) st R is closed holds
F1 " R is closed then A37: F1 is continuous ;
reconsider Q19 = Q1, Q29 = Q2 as non empty Subset of (TOP-REAL 2) ;
consider ff being Function of I[01],((TOP-REAL 2) | Q1) such that
A38: ff is being_homeomorphism and
ff . 0 = q1 and
ff . 1 = q2 by A25, TOPREAL1:def 1;
A39: rng ff = [#] ((TOP-REAL 2) | Q1) by A38;
A40: rng (f | Q2) = P2 by RELAT_1:115
.= [#] ((TOP-REAL 2) | P2) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2) | P2) ;
A41: p2 = f . q2 by A12, A14, A16, A18, FUNCT_1:35;
dom (f | Q2) = R^2-unit_square /\ Q2 by A22, A9, RELAT_1:61
.= Q2 by A27, XBOOLE_1:21
.= [#] ((TOP-REAL 2) | Q2) by PRE_TOPC:def 5 ;
then reconsider F2 = f | Q2 as Function of ((TOP-REAL 2) | Q2),((TOP-REAL 2) | P2) by A40, FUNCT_2:def 1, RELSET_1:4;
A42: f " P2 c= Q2 by A12, FUNCT_1:82;
[#] ((TOP-REAL 2) | Q2) = Q2 by PRE_TOPC:def 5;
then A43: (TOP-REAL 2) | Q2 is SubSpace of (TOP-REAL 2) | R^2-unit_square by A9, A27, TOPMETR:3, XBOOLE_1:7;
Q2 c= f " P2 by A22, A9, A27, FUNCT_1:76, XBOOLE_1:7;
then A44: f " P2 = Q2 by A42, XBOOLE_0:def 10;
for R being Subset of ((TOP-REAL 2) | P2) st R is closed holds
F2 " R is closed then A48: F2 is continuous ;
A49: q2 in {q1,q2} by TARSKI:def 2;
A50: q1 in {q1,q2} by TARSKI:def 2;
A51: q1 in {q1,q2} by TARSKI:def 2;
{q1,q2} c= Q1 by A28, XBOOLE_1:17;
then A52: q1 in (dom f) /\ Q1 by A15, A19, A51, XBOOLE_0:def 4;
take P1 ; :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 ; :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A53: (TOP-REAL 2) | P1 is T_2 by TOPMETR:2;
A54: q2 in {q1,q2} by TARSKI:def 2;
{q1,q2} c= Q1 by A28, XBOOLE_1:17;
then A55: q2 in (dom f) /\ Q1 by A15, A20, A54, XBOOLE_0:def 4;
A56: p2 = f . q2 by A12, A14, A16, A18, FUNCT_1:35
.= F1 . q2 by A55, FUNCT_1:48 ;
A57: rng F1 = [#] ((TOP-REAL 2) | P1) by A30;
ff is continuous by A38;
then A58: (TOP-REAL 2) | Q19 is compact by A11, A39, COMPTS_1:14;
A59: F1 is one-to-one by A12, FUNCT_1:52;
p1 = f . q1 by A12, A14, A16, A17, FUNCT_1:35
.= F1 . q1 by A52, FUNCT_1:48 ;
hence P1 is_an_arc_of p1,p2 by A25, A57, A59, A37, A58, A53, A56, Th3, COMPTS_1:17; :: thesis: ( P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A60: (TOP-REAL 2) | P2 is T_2 by TOPMETR:2;
consider ff being Function of I[01],((TOP-REAL 2) | Q2) such that
A61: ff is being_homeomorphism and
ff . 0 = q1 and
ff . 1 = q2 by A26, TOPREAL1:def 1;
A62: rng ff = [#] ((TOP-REAL 2) | Q2) by A61;
{q1,q2} c= Q2 by A28, XBOOLE_1:17;
then q1 in (dom f) /\ Q2 by A15, A19, A50, XBOOLE_0:def 4;
then A63: p1 = F2 . q1 by A24, FUNCT_1:48;
A64: F2 is one-to-one by A12, FUNCT_1:52;
{q1,q2} c= Q2 by A28, XBOOLE_1:17;
then q2 in (dom f) /\ Q2 by A15, A20, A49, XBOOLE_0:def 4;
then A65: p2 = F2 . q2 by A41, FUNCT_1:48;
ff is continuous by A61;
then A66: (TOP-REAL 2) | Q29 is compact by A11, A62, COMPTS_1:14;
rng F2 = [#] ((TOP-REAL 2) | P2) by A40;
hence P2 is_an_arc_of p1,p2 by A26, A64, A48, A66, A60, A63, A65, Th3, COMPTS_1:17; :: thesis: ( P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
[#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 5;
hence P = f .: (Q1 \/ Q2) by A13, A3, A9, A27, RELAT_1:113
.= P1 \/ P2 by RELAT_1:120 ;
:: thesis: P1 /\ P2 = {p1,p2}
thus P1 /\ P2 = f .: (Q1 /\ Q2) by A12, FUNCT_1:62
.= f .: ({q1} \/ {q2}) by A28, ENUMSET1:1
.= (Im (f,q1)) \/ (Im (f,q2)) by RELAT_1:120
.= {p1} \/ (Im (f,q2)) by A15, A19, A24, FUNCT_1:59
.= {p1} \/ {p2} by A15, A20, A41, FUNCT_1:59
.= {p1,p2} by ENUMSET1:1 ; :: thesis: verum