let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve implies ( W-min P in Lower_Arc P & E-max P in Lower_Arc P & W-min P in Upper_Arc P & E-max P in Upper_Arc P ) )
assume P is being_simple_closed_curve ; :: thesis: ( W-min P in Lower_Arc P & E-max P in Lower_Arc P & W-min P in Upper_Arc P & E-max P in Upper_Arc P )
then ( Upper_Arc P is_an_arc_of W-min P, E-max P & Lower_Arc P is_an_arc_of E-max P, W-min P ) by JORDAN6:50;
hence ( W-min P in Lower_Arc P & E-max P in Lower_Arc P & W-min P in Upper_Arc P & E-max P in Upper_Arc P ) by TOPREAL1:1; :: thesis: verum