theorem Th17: :: JORDAN_A:17
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st p <> q & LE p,q,C holds
Segment (p,q,C) is_an_arc_of p,q