for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
( 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 )