let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } implies ( Upper_Arc P c= P & Lower_Arc P c= P ) )
assume P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ; :: thesis: ( Upper_Arc P c= P & Lower_Arc P c= P )
then P is being_simple_closed_curve by JGRAPH_3:26;
hence ( Upper_Arc P c= P & Lower_Arc P c= P ) by JORDAN6:61; :: thesis: verum