let P be non empty Subset of (); :: thesis: ( P is being_simple_closed_curve iff ( ex p1, p2 being Point of () st
( p1 <> p2 & p1 in P & p2 in P ) & ( for p1, p2 being Point of () st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being non empty Subset of () st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ) ) )

thus ( P is being_simple_closed_curve implies ( ex p1, p2 being Point of () st
( p1 <> p2 & p1 in P & p2 in P ) & ( for p1, p2 being Point of () st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being non empty Subset of () st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ) ) ) :: thesis: ( ex p1, p2 being Point of () st
( p1 <> p2 & p1 in P & p2 in P ) & ( for p1, p2 being Point of () st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being non empty Subset of () st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ) implies P is being_simple_closed_curve )
proof
assume A1: P is being_simple_closed_curve ; :: thesis: ( ex p1, p2 being Point of () st
( p1 <> p2 & p1 in P & p2 in P ) & ( for p1, p2 being Point of () st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being non empty Subset of () 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 (),(() | P) such that
A2: f is being_homeomorphism ;
A3: dom f = [#] () by A2;
A4: [#] (() | P) c= [#] () by PRE_TOPC:def 4;
A5: f is continuous by A2;
thus ex p1, p2 being Point of () st
( p1 <> p2 & p1 in P & p2 in P ) by ; :: thesis: for p1, p2 being Point of () st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being non empty Subset of () 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 (); :: thesis: ( p1 <> p2 & p1 in P & p2 in P implies ex P1, P2 being non empty Subset of () 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 () st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )

A9: [#] () = R^2-unit_square by PRE_TOPC:def 5;
set q1 = (f ") . p1;
set q2 = (f ") . p2;
A10: [#] () c= [#] () by PRE_TOPC:def 4;
A11: I is compact by ;
A12: f is one-to-one by A2;
A13: rng f = [#] (() | P) by A2;
then f is onto by FUNCT_2:def 3;
then A14: f " = f " by ;
then A15: rng (f ") = dom f by ;
A16: dom (f ") = rng f by ;
then A17: p1 in dom (f ") by ;
A18: p2 in dom (f ") by ;
reconsider f = f as Function of (),(() | P) ;
A19: (f ") . p1 in rng (f ") by ;
A20: (f ") . p2 in rng (f ") by ;
reconsider q1 = (f ") . p1, q2 = (f ") . p2 as Point of () by ;
A21: q1 <> q2 by ;
A22: dom f = the carrier of () by FUNCT_2:def 1;
then A23: q2 in R^2-unit_square by ;
A24: p1 = f . q1 by ;
q1 in R^2-unit_square by ;
then consider Q1, Q2 being non empty Subset of () 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 ;
A29: Q2 c= dom f by ;
set P1 = f .: Q1;
set P2 = f .: Q2;
Q1 c= dom f by ;
then reconsider P1 = f .: Q1, P2 = f .: Q2 as non empty Subset of () by ;
A30: rng (f | Q1) = P1 by RELAT_1:115
.= [#] (() | P1) by PRE_TOPC:def 5
.= the carrier of (() | P1) ;
dom (f | Q1) = R^2-unit_square /\ Q1 by
.= Q1 by
.= [#] (() | Q1) by PRE_TOPC:def 5 ;
then reconsider F1 = f | Q1 as Function of (() | Q1),(() | P1) by ;
A31: f " P1 c= Q1 by ;
[#] (() | Q1) = Q1 by PRE_TOPC:def 5;
then A32: (TOP-REAL 2) | Q1 is SubSpace of () | R^2-unit_square by ;
Q1 c= f " P1 by ;
then A33: f " P1 = Q1 by ;
for R being Subset of (() | P1) st R is closed holds
F1 " R is closed
proof
let R be Subset of (() | P1); :: thesis: ( R is closed implies F1 " R is closed )
assume R is closed ; :: thesis: F1 " R is closed
then consider S1 being Subset of () such that
A34: S1 is closed and
A35: R = S1 /\ ([#] (() | P1)) by PRE_TOPC:13;
S1 /\ (rng f) is Subset of (() | P) ;
then reconsider S2 = (rng f) /\ S1 as Subset of (() | P) ;
S2 is closed by ;
then A36: f " S2 is closed by A5;
F1 " R = Q1 /\ (f " R) by FUNCT_1:70
.= Q1 /\ ((f " S1) /\ (f " ([#] (() | P1)))) by
.= ((f " S1) /\ Q1) /\ Q1 by
.= (f " S1) /\ (Q1 /\ Q1) by XBOOLE_1:16
.= (f " S1) /\ ([#] (() | Q1)) by PRE_TOPC:def 5
.= (f " ((rng f) /\ S1)) /\ ([#] (() | Q1)) by RELAT_1:133 ;
hence F1 " R is closed by ; :: thesis: verum
end;
then A37: F1 is continuous ;
reconsider Q19 = Q1, Q29 = Q2 as non empty Subset of () ;
consider ff being Function of I,(() | Q1) such that
A38: ff is being_homeomorphism and
ff . 0 = q1 and
ff . 1 = q2 by ;
A39: rng ff = [#] (() | Q1) by A38;
A40: rng (f | Q2) = P2 by RELAT_1:115
.= [#] (() | P2) by PRE_TOPC:def 5
.= the carrier of (() | P2) ;
A41: p2 = f . q2 by ;
dom (f | Q2) = R^2-unit_square /\ Q2 by
.= Q2 by
.= [#] (() | Q2) by PRE_TOPC:def 5 ;
then reconsider F2 = f | Q2 as Function of (() | Q2),(() | P2) by ;
A42: f " P2 c= Q2 by ;
[#] (() | Q2) = Q2 by PRE_TOPC:def 5;
then A43: (TOP-REAL 2) | Q2 is SubSpace of () | R^2-unit_square by ;
Q2 c= f " P2 by ;
then A44: f " P2 = Q2 by ;
for R being Subset of (() | P2) st R is closed holds
F2 " R is closed
proof
let R be Subset of (() | P2); :: thesis: ( R is closed implies F2 " R is closed )
assume R is closed ; :: thesis: F2 " R is closed
then consider S1 being Subset of () such that
A45: S1 is closed and
A46: R = S1 /\ ([#] (() | P2)) by PRE_TOPC:13;
S1 /\ (rng f) is Subset of (() | P) ;
then reconsider S2 = (rng f) /\ S1 as Subset of (() | P) ;
S2 is closed by ;
then A47: f " S2 is closed by A5;
F2 " R = Q2 /\ (f " R) by FUNCT_1:70
.= Q2 /\ ((f " S1) /\ (f " ([#] (() | P2)))) by
.= ((f " S1) /\ Q2) /\ Q2 by
.= (f " S1) /\ (Q2 /\ Q2) by XBOOLE_1:16
.= (f " S1) /\ ([#] (() | Q2)) by PRE_TOPC:def 5
.= (f " ((rng f) /\ S1)) /\ ([#] (() | Q2)) by RELAT_1:133 ;
hence F2 " R is closed by ; :: thesis: verum
end;
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 ;
then A52: q1 in (dom f) /\ Q1 by ;
take P1 ; :: thesis: ex P2 being non empty Subset of () 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 ;
then A55: q2 in (dom f) /\ Q1 by ;
A56: p2 = f . q2 by
.= F1 . q2 by ;
A57: rng F1 = [#] (() | P1) by A30;
ff is continuous by A38;
then A58: (TOP-REAL 2) | Q19 is compact by ;
A59: F1 is one-to-one by ;
p1 = f . q1 by
.= F1 . q1 by ;
hence P1 is_an_arc_of p1,p2 by ; :: 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,(() | Q2) such that
A61: ff is being_homeomorphism and
ff . 0 = q1 and
ff . 1 = q2 by ;
A62: rng ff = [#] (() | Q2) by A61;
{q1,q2} c= Q2 by ;
then q1 in (dom f) /\ Q2 by ;
then A63: p1 = F2 . q1 by ;
A64: F2 is one-to-one by ;
{q1,q2} c= Q2 by ;
then q2 in (dom f) /\ Q2 by ;
then A65: p2 = F2 . q2 by ;
ff is continuous by A61;
then A66: (TOP-REAL 2) | Q29 is compact by ;
rng F2 = [#] (() | P2) by A40;
hence P2 is_an_arc_of p1,p2 by ; :: thesis: ( P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
[#] (() | P) = P by PRE_TOPC:def 5;
hence P = f .: (Q1 \/ Q2) by
.= P1 \/ P2 by RELAT_1:120 ;
:: thesis: P1 /\ P2 = {p1,p2}
thus P1 /\ P2 = f .: (Q1 /\ Q2) by
.= f .: ({q1} \/ {q2}) by
.= (Im (f,q1)) \/ (Im (f,q2)) by RELAT_1:120
.= {p1} \/ (Im (f,q2)) by
.= {p1} \/ {p2} by
.= {p1,p2} by ENUMSET1:1 ; :: thesis: verum
end;
given p1, p2 being Point of () such that A67: p1 <> p2 and
A68: p1 in P and
A69: p2 in P ; :: thesis: ( ex p1, p2 being Point of () st
( p1 <> p2 & p1 in P & p2 in P & ( for P1, P2 being non empty Subset of () holds
( not P1 is_an_arc_of p1,p2 or not P2 is_an_arc_of p1,p2 or not P = P1 \/ P2 or not P1 /\ P2 = {p1,p2} ) ) ) or P is being_simple_closed_curve )

assume for p1, p2 being Point of () st p1 <> p2 & p1 in P & p2 in P holds
ex P1, P2 being non empty Subset of () 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 () st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) by ;
hence P is being_simple_closed_curve by Lm34; :: thesis: verum