theorem Th13: :: JORDAN_A:13

for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st LE p, E-max C,C holds
Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)))