theorem Th40: :: JGRAPH_5:40

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds
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 )