for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
( Segment ((W-min P),(E-max P),P) = Upper_Arc P & Segment ((E-max P),(W-min P),P) = Lower_Arc P )