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

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: ( 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} ) ) implies P is being_simple_closed_curve )

A68: p1 in P and

A69: p2 in P ; :: thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st

( p1 <> p2 & p1 in P & p2 in P & ( for P1, P2 being non empty Subset of (TOP-REAL 2) 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 (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: P is being_simple_closed_curve

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 A67, A68, A69;

hence P is being_simple_closed_curve by Lm34; :: thesis: verum

( 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} ) ) ) )

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: ( 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} ) ) implies P is being_simple_closed_curve )

proof

given p1, p2 being Point of (TOP-REAL 2) such that A67:
p1 <> p2
and
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

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

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

end;( 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

proof

then A37:
F1 is continuous
;
let R be Subset of ((TOP-REAL 2) | 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 (TOP-REAL 2) such that

A34: S1 is closed and

A35: R = S1 /\ ([#] ((TOP-REAL 2) | P1)) by PRE_TOPC:13;

S1 /\ (rng f) is Subset of ((TOP-REAL 2) | P) ;

then reconsider S2 = (rng f) /\ S1 as Subset of ((TOP-REAL 2) | P) ;

S2 is closed by A13, A34, PRE_TOPC:13;

then A36: f " S2 is closed by A5;

F1 " R = Q1 /\ (f " R) by FUNCT_1:70

.= Q1 /\ ((f " S1) /\ (f " ([#] ((TOP-REAL 2) | P1)))) by A35, FUNCT_1:68

.= ((f " S1) /\ Q1) /\ Q1 by A33, PRE_TOPC:def 5

.= (f " S1) /\ (Q1 /\ Q1) by XBOOLE_1:16

.= (f " S1) /\ ([#] ((TOP-REAL 2) | Q1)) by PRE_TOPC:def 5

.= (f " ((rng f) /\ S1)) /\ ([#] ((TOP-REAL 2) | Q1)) by RELAT_1:133 ;

hence F1 " R is closed by A32, A36, PRE_TOPC:13; :: thesis: verum

end;assume R is closed ; :: thesis: F1 " R is closed

then consider S1 being Subset of (TOP-REAL 2) such that

A34: S1 is closed and

A35: R = S1 /\ ([#] ((TOP-REAL 2) | P1)) by PRE_TOPC:13;

S1 /\ (rng f) is Subset of ((TOP-REAL 2) | P) ;

then reconsider S2 = (rng f) /\ S1 as Subset of ((TOP-REAL 2) | P) ;

S2 is closed by A13, A34, PRE_TOPC:13;

then A36: f " S2 is closed by A5;

F1 " R = Q1 /\ (f " R) by FUNCT_1:70

.= Q1 /\ ((f " S1) /\ (f " ([#] ((TOP-REAL 2) | P1)))) by A35, FUNCT_1:68

.= ((f " S1) /\ Q1) /\ Q1 by A33, PRE_TOPC:def 5

.= (f " S1) /\ (Q1 /\ Q1) by XBOOLE_1:16

.= (f " S1) /\ ([#] ((TOP-REAL 2) | Q1)) by PRE_TOPC:def 5

.= (f " ((rng f) /\ S1)) /\ ([#] ((TOP-REAL 2) | Q1)) by RELAT_1:133 ;

hence F1 " R is closed by A32, A36, PRE_TOPC:13; :: thesis: verum

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

proof

then A48:
F2 is continuous
;
let R be Subset of ((TOP-REAL 2) | 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 (TOP-REAL 2) such that

A45: S1 is closed and

A46: R = S1 /\ ([#] ((TOP-REAL 2) | P2)) by PRE_TOPC:13;

S1 /\ (rng f) is Subset of ((TOP-REAL 2) | P) ;

then reconsider S2 = (rng f) /\ S1 as Subset of ((TOP-REAL 2) | P) ;

S2 is closed by A13, A45, PRE_TOPC:13;

then A47: f " S2 is closed by A5;

F2 " R = Q2 /\ (f " R) by FUNCT_1:70

.= Q2 /\ ((f " S1) /\ (f " ([#] ((TOP-REAL 2) | P2)))) by A46, FUNCT_1:68

.= ((f " S1) /\ Q2) /\ Q2 by A44, PRE_TOPC:def 5

.= (f " S1) /\ (Q2 /\ Q2) by XBOOLE_1:16

.= (f " S1) /\ ([#] ((TOP-REAL 2) | Q2)) by PRE_TOPC:def 5

.= (f " ((rng f) /\ S1)) /\ ([#] ((TOP-REAL 2) | Q2)) by RELAT_1:133 ;

hence F2 " R is closed by A43, A47, PRE_TOPC:13; :: thesis: verum

end;assume R is closed ; :: thesis: F2 " R is closed

then consider S1 being Subset of (TOP-REAL 2) such that

A45: S1 is closed and

A46: R = S1 /\ ([#] ((TOP-REAL 2) | P2)) by PRE_TOPC:13;

S1 /\ (rng f) is Subset of ((TOP-REAL 2) | P) ;

then reconsider S2 = (rng f) /\ S1 as Subset of ((TOP-REAL 2) | P) ;

S2 is closed by A13, A45, PRE_TOPC:13;

then A47: f " S2 is closed by A5;

F2 " R = Q2 /\ (f " R) by FUNCT_1:70

.= Q2 /\ ((f " S1) /\ (f " ([#] ((TOP-REAL 2) | P2)))) by A46, FUNCT_1:68

.= ((f " S1) /\ Q2) /\ Q2 by A44, PRE_TOPC:def 5

.= (f " S1) /\ (Q2 /\ Q2) by XBOOLE_1:16

.= (f " S1) /\ ([#] ((TOP-REAL 2) | Q2)) by PRE_TOPC:def 5

.= (f " ((rng f) /\ S1)) /\ ([#] ((TOP-REAL 2) | Q2)) by RELAT_1:133 ;

hence F2 " R is closed by A43, A47, PRE_TOPC:13; :: thesis: verum

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

A68: p1 in P and

A69: p2 in P ; :: thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st

( p1 <> p2 & p1 in P & p2 in P & ( for P1, P2 being non empty Subset of (TOP-REAL 2) 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 (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: P is being_simple_closed_curve

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 A67, A68, A69;

hence P is being_simple_closed_curve by Lm34; :: thesis: verum