theorem :: JORDAN21:23

for C being Simple_closed_curve
for P being connected compact Subset of (TOP-REAL 2) st P c= C & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P