theorem :: TOPMETR3:15

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