let P be non empty Subset of (TOP-REAL 2); :: thesis:
thus ( P is being_simple_closed_curve implies ( 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} ) ) ) ) :: thesis:

proof

assume A1: P is being_simple_closed_curve ; :: thesis:
then consider f being Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | P) such that
A2: f is being_homeomorphism by Def1;
thus ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) by A1, Th4; :: thesis:
let p1, p2 be Point of (TOP-REAL 2); :: thesis:
assume that
A3: p1 <> p2 and
A4: p1 in P and
A5: p2 in P ; :: thesis:
A6: f is one-to-one by A2, TOPS_2:def 5;
A7: f is continuous by A2, TOPS_2:def 5;
A8: ( rng f = [#] ((TOP-REAL 2) | P) & dom f = [#] ((TOP-REAL 2) | R^2-unit_square ) ) by A2, TOPS_2:def 5;
then A9: f " = f " by A6, TOPS_2:def 4;
then A10: dom (f " ) = rng f by A6, FUNCT_1:54;
A11: f " is one-to-one by A6, A9;
A12: rng (f " ) = dom f by A6, A9, FUNCT_1:55;
A13: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 10;
A14: ( p1 in dom (f " ) & p2 in dom (f " ) ) by A4, A5, A8, A10, PRE_TOPC:def 10;
set q1 = (f " ) . p1;
set q2 = (f " ) . p2;
set RS = R^2-unit_square ;
reconsider f = f as Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | P) ;
A15: ( [#] ((TOP-REAL 2) | R^2-unit_square ) c= [#] (TOP-REAL 2) & rng (f " ) = [#] ((TOP-REAL 2) | R^2-unit_square ) & (f " ) . p1 in rng (f " ) & (f " ) . p2 in rng (f " ) ) by A12, A14, FUNCT_1:def 5, FUNCT_2:def 1, PRE_TOPC:def 9;
then reconsider q1 = (f " ) . p1, q2 = (f " ) . p2 as Point of (TOP-REAL 2) ;
A16: q1 <> q2 by A3, A11, A14, FUNCT_1:def 8;
A17: dom f = the carrier of ((TOP-REAL 2) | R^2-unit_square ) by FUNCT_2:def 1;
A18: [#] ((TOP-REAL 2) | R^2-unit_square ) = R^2-unit_square by PRE_TOPC:def 10;
then ( q1 in R^2-unit_square & q2 in R^2-unit_square ) by A12, A14, A17, FUNCT_1:def 5;
then consider Q1, Q2 being non empty Subset of (TOP-REAL 2) such that
A19: ( Q1 is_an_arc_of q1,q2 & Q2 is_an_arc_of q1,q2 ) and
A20: ( R^2-unit_square = Q1 \/ Q2 & Q1 /\ Q2 = {q1,q2} ) by A16, Th1;
set P1 = f .: Q1;
set P2 = f .: Q2;
A21: ( Q1 c= dom f & Q2 c= dom f ) by A17, A18, A20, XBOOLE_1:7;
( f .: Q1 c= rng f & f .: Q2 c= rng f & [#] ((TOP-REAL 2) | P) c= [#] (TOP-REAL 2) ) by PRE_TOPC:def 9, RELAT_1:144;
then reconsider P1 = f .: Q1, P2 = f .: Q2 as non empty Subset of (TOP-REAL 2) by A21, XBOOLE_1:1;
take P1 ; :: thesis:
take P2 ; :: thesis:
A22: rng (f | Q1) = P1 by RELAT_1:148
.= [#] ((TOP-REAL 2) | P1) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | P1) ;
A23: dom (f | Q1) = R^2-unit_square /\ Q1 by A17, A18, RELAT_1:90
.= Q1 by A20, XBOOLE_1:21
.= [#] ((TOP-REAL 2) | Q1) by PRE_TOPC:def 10 ;
then reconsider F1 = f | Q1 as Function of ((TOP-REAL 2) | Q1),((TOP-REAL 2) | P1) by A22, FUNCT_2:def 1, RELSET_1:11;
[#] ((TOP-REAL 2) | Q1) = Q1 by PRE_TOPC:def 10;
then A24: (TOP-REAL 2) | Q1 is SubSpace of (TOP-REAL 2) | R^2-unit_square by A18, A20, TOPMETR:4, XBOOLE_1:7;
A25: rng F1 = [#] ((TOP-REAL 2) | P1) by A22;
A26: F1 is one-to-one by A6, FUNCT_1:84;
( Q1 c= f " P1 & Q2 c= f " P2 & f " P1 c= Q1 & f " P2 c= Q2 ) by A6, A17, A18, A20, FUNCT_1:146, FUNCT_1:152, XBOOLE_1:7;
then A27: ( f " P1 = Q1 & f " P2 = Q2 ) by XBOOLE_0:def 10;
for R being Subset of ((TOP-REAL 2) | P1) st R is closed holds
F1 " R is closed

proof

let R be Subset of ((TOP-REAL 2) | P1); :: thesis:
assume R is closed ; :: thesis:
then consider S1 being Subset of (TOP-REAL 2) such that
A28: S1 is closed and
A29: R = S1 /\ ([#] ((TOP-REAL 2) | P1)) by PRE_TOPC:43;
S1 /\ (rng f) is Subset of ((TOP-REAL 2) | P) ;
then reconsider S2 = (rng f) /\ S1 as Subset of ((TOP-REAL 2) | P) ;
A30: F1 " R = Q1 /\ (f " R) by FUNCT_1:139
.= Q1 /\ ((f " S1) /\ (f " ([#] ((TOP-REAL 2) | P1)))) by A29, FUNCT_1:137
.= ((f " S1) /\ Q1) /\ Q1 by A27, PRE_TOPC:def 10
.= (f " S1) /\ (Q1 /\ Q1) by XBOOLE_1:16
.= (f " S1) /\ ([#] ((TOP-REAL 2) | Q1)) by PRE_TOPC:def 10
.= (f " ((rng f) /\ S1)) /\ ([#] ((TOP-REAL 2) | Q1)) by RELAT_1:168 ;
S2 is closed by A8, A28, PRE_TOPC:43;
then f " S2 is closed by A7, PRE_TOPC:def 12;
hence F1 " R is closed by A24, A30, PRE_TOPC:43; :: thesis:

end;

then A31: F1 is continuous by PRE_TOPC:def 12;
consider ff being Function of I[01] ,((TOP-REAL 2) | Q1) such that
A32: ff is being_homeomorphism and
( ff . 0 = q1 & ff . 1 = q2 ) by A19, TOPREAL1:def 2;
A33: I[01] is compact by HEINE:11, TOPMETR:27;
reconsider Q1' = Q1, Q2' = Q2 as non empty Subset of (TOP-REAL 2) ;
( ff is continuous & rng ff = [#] ((TOP-REAL 2) | Q1) ) by A32, TOPS_2:def 5;
then A34: (TOP-REAL 2) | Q1' is compact by A33, COMPTS_1:23;
A35: (TOP-REAL 2) | P1 is T_2 by TOPMETR:3;
( q1 in {q1,q2} & {q1,q2} c= Q1 ) by A20, TARSKI:def 2, XBOOLE_1:17;
then A36: q1 in (dom f) /\ Q1 by A12, A15, XBOOLE_0:def 4;
A37: p1 = f . q1 by A6, A9, A10, A14, FUNCT_1:57
.= F1 . q1 by A36, FUNCT_1:71 ;
( q2 in {q1,q2} & {q1,q2} c= Q1 ) by A20, TARSKI:def 2, XBOOLE_1:17;
then A38: q2 in (dom f) /\ Q1 by A12, A15, XBOOLE_0:def 4;
p2 = f . q2 by A6, A9, A10, A14, FUNCT_1:57
.= F1 . q2 by A38, FUNCT_1:71 ;
hence P1 is_an_arc_of p1,p2 by A19, A23, A25, A26, A31, A34, A35, A37, Th3, COMPTS_1:26; :: thesis:
A39: rng (f | Q2) = P2 by RELAT_1:148
.= [#] ((TOP-REAL 2) | P2) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | P2) ;
A40: dom (f | Q2) = R^2-unit_square /\ Q2 by A17, A18, RELAT_1:90
.= Q2 by A20, XBOOLE_1:21
.= [#] ((TOP-REAL 2) | Q2) by PRE_TOPC:def 10 ;
then reconsider F2 = f | Q2 as Function of ((TOP-REAL 2) | Q2),((TOP-REAL 2) | P2) by A39, FUNCT_2:def 1, RELSET_1:11;
[#] ((TOP-REAL 2) | Q2) = Q2 by PRE_TOPC:def 10;
then A41: (TOP-REAL 2) | Q2 is SubSpace of (TOP-REAL 2) | R^2-unit_square by A18, A20, TOPMETR:4, XBOOLE_1:7;
A42: rng F2 = [#] ((TOP-REAL 2) | P2) by A39;
A43: F2 is one-to-one by A6, FUNCT_1:84;
for R being Subset of ((TOP-REAL 2) | P2) st R is closed holds
F2 " R is closed

proof

let R be Subset of ((TOP-REAL 2) | P2); :: thesis:
assume R is closed ; :: thesis:
then consider S1 being Subset of (TOP-REAL 2) such that
A44: S1 is closed and
A45: R = S1 /\ ([#] ((TOP-REAL 2) | P2)) by PRE_TOPC:43;
S1 /\ (rng f) is Subset of ((TOP-REAL 2) | P) ;
then reconsider S2 = (rng f) /\ S1 as Subset of ((TOP-REAL 2) | P) ;
A46: F2 " R = Q2 /\ (f " R) by FUNCT_1:139
.= Q2 /\ ((f " S1) /\ (f " ([#] ((TOP-REAL 2) | P2)))) by A45, FUNCT_1:137
.= ((f " S1) /\ Q2) /\ Q2 by A27, PRE_TOPC:def 10
.= (f " S1) /\ (Q2 /\ Q2) by XBOOLE_1:16
.= (f " S1) /\ ([#] ((TOP-REAL 2) | Q2)) by PRE_TOPC:def 10
.= (f " ((rng f) /\ S1)) /\ ([#] ((TOP-REAL 2) | Q2)) by RELAT_1:168 ;
S2 is closed by A8, A44, PRE_TOPC:43;
then f " S2 is closed by A7, PRE_TOPC:def 12;
hence F2 " R is closed by A41, A46, PRE_TOPC:43; :: thesis:

end;

then A47: F2 is continuous by PRE_TOPC:def 12;
consider ff being Function of I[01] ,((TOP-REAL 2) | Q2) such that
A48: ff is being_homeomorphism and
( ff . 0 = q1 & ff . 1 = q2 ) by A19, TOPREAL1:def 2;
( ff is continuous & rng ff = [#] ((TOP-REAL 2) | Q2) ) by A48, TOPS_2:def 5;
then A49: (TOP-REAL 2) | Q2' is compact by A33, COMPTS_1:23;
A50: (TOP-REAL 2) | P2 is T_2 by TOPMETR:3;
( q1 in {q1,q2} & {q1,q2} c= Q2 ) by A20, TARSKI:def 2, XBOOLE_1:17;
then A51: q1 in (dom f) /\ Q2 by A12, A15, XBOOLE_0:def 4;
A52: p1 = f . q1 by A6, A9, A10, A14, FUNCT_1:57;
then A53: p1 = F2 . q1 by A51, FUNCT_1:71;
( q2 in {q1,q2} & {q1,q2} c= Q2 ) by A20, TARSKI:def 2, XBOOLE_1:17;
then A54: q2 in (dom f) /\ Q2 by A12, A15, XBOOLE_0:def 4;
A55: p2 = f . q2 by A6, A9, A10, A14, FUNCT_1:57;
then p2 = F2 . q2 by A54, FUNCT_1:71;
hence P2 is_an_arc_of p1,p2 by A19, A40, A42, A43, A47, A49, A50, A53, Th3, COMPTS_1:26; :: thesis:
thus P = f .: (Q1 \/ Q2) by A8, A13, A18, A20, RELAT_1:146
.= P1 \/ P2 by RELAT_1:153 ; :: thesis:
thus P1 /\ P2 = f .: (Q1 /\ Q2) by A6, FUNCT_1:121
.= f .: ({q1} \/ {q2}) by A20, ENUMSET1:41
.= (Im f,q1) \/ (Im f,q2) by RELAT_1:153
.= {p1} \/ (Im f,q2) by A12, A15, A52, FUNCT_1:117
.= {p1} \/ {p2} by A12, A15, A55, FUNCT_1:117
.= {p1,p2} by ENUMSET1:41 ; :: thesis:

end;

given p1, p2 being Point of (TOP-REAL 2) such that A56: ( p1 <> p2 & p1 in P & p2 in P ) ; :: thesis:
assume 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} ) ; :: thesis:
then 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} ) by A56;
hence P is being_simple_closed_curve by A56, Lm27; :: thesis: