theorem Th8: :: JORDAN_A:8
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE q, E-max C,C & p <> q holds
Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q)