theorem Th6: :: JORDAN_A:6

for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds
LE q, E-max C,C