for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} )