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