theorem Th5: :: JORDAN_A:5

for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st q in Lower_Arc C & q <> W-min C holds
LE E-max C,q,C