theorem Th11: :: JORDAN_A:11

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