theorem Th9: :: JORDAN_A:9

for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds
Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q)