theorem :: JORDAN16:19

for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in C holds
( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) )