let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ex f being Function of (Closed-Interval-TSpace (- 1),1),((TOP-REAL 2) | (Lower_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
f . (q `1 ) = q ) & f . (- 1) = W-min P & f . 1 = E-max P ) )
assume A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } ; :: thesis: ex f being Function of (Closed-Interval-TSpace (- 1),1),((TOP-REAL 2) | (Lower_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
f . (q `1 ) = q ) & f . (- 1) = W-min P & f . 1 = E-max P )
then A2: P is being_simple_closed_curve by JGRAPH_3:36;
then A3: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;
set P4 = Lower_Arc P;
A4: ( Lower_Arc P is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) by A2, JORDAN6:def 9;
reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
set K0 = Lower_Arc P;
reconsider g2 = g | (Lower_Arc P) as Function of ((TOP-REAL 2) | (Lower_Arc P)),R^1 by PRE_TOPC:30;
A5: for p being Point of ((TOP-REAL 2) | (Lower_Arc P)) holds g2 . p = proj1 . p

proof

let p be Point of ((TOP-REAL 2) | (Lower_Arc P)); :: thesis: g2 . p = proj1 . p
p in the carrier of ((TOP-REAL 2) | (Lower_Arc P)) ;
then p in Lower_Arc P by PRE_TOPC:29;
hence g2 . p = proj1 . p by FUNCT_1:72; :: thesis: verum

end;

reconsider g3 = g2 as continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace (- 1),1) by A1, Lm4;
E-max P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A6: E-max P in Lower_Arc P by A4, XBOOLE_0:def 4;
W-min P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A7: W-min P in Lower_Arc P by A4, XBOOLE_0:def 4;
A8: dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;
then A9: dom g3 = Lower_Arc P by PRE_TOPC:def 10;
A10: rng g3 = [#] (Closed-Interval-TSpace (- 1),1) by A1, Lm4;
A11: g3 is one-to-one by A1, Lm4;
( not Lower_Arc P is empty & Lower_Arc P is compact ) by A3, JORDAN5A:1;
then A12: (TOP-REAL 2) | (Lower_Arc P) is compact ;
Closed-Interval-TSpace (- 1),1 = TopSpaceMetr (Closed-Interval-MSpace (- 1),1) by TOPMETR:def 8;
then Closed-Interval-TSpace (- 1),1 is T_2 by PCOMPS_1:38;
then A13: g3 /" is being_homeomorphism by A8, A10, A11, A12, COMPTS_1:26, TOPS_2:70;
A14: for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
(g3 /" ) . (q `1 ) = q

proof

let q be Point of (TOP-REAL 2); :: thesis: ( q in Lower_Arc P implies (g3 /" ) . (q `1 ) = q )
assume A15: q in Lower_Arc P ; :: thesis: (g3 /" ) . (q `1 ) = q
reconsider g4 = g3 as Function ;
A16: ( q in dom g4 implies ( q = (g4 " ) . (g4 . q) & q = ((g4 " ) * g4) . q ) ) by A11, FUNCT_1:56;
g3 . q = proj1 . q by A5, A9, A15
.= q `1 by PSCOMP_1:def 28 ;
hence (g3 /" ) . (q `1 ) = q by A8, A10, A11, A15, A16, PRE_TOPC:def 10, TOPS_2:def 4; :: thesis: verum

end;

A17: W-min P = |[(- 1),0 ]| by A1, Th32;
A18: (g3 /" ) . (- 1) = (g3 /" ) . (|[(- 1),0 ]| `1 ) by EUCLID:56
.= W-min P by A7, A14, A17 ;
A19: E-max P = |[1,0 ]| by A1, Th33;
(g3 /" ) . 1 = (g3 /" ) . (|[1,0 ]| `1 ) by EUCLID:56
.= E-max P by A6, A14, A19 ;
hence ex f being Function of (Closed-Interval-TSpace (- 1),1),((TOP-REAL 2) | (Lower_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
f . (q `1 ) = q ) & f . (- 1) = W-min P & f . 1 = E-max P ) by A13, A14, A18; :: thesis: verum