theorem Th16: :: JORDAN_A:16
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in C & p <> W-min C holds
Segment (p,(W-min C),C) is_an_arc_of p, W-min C