theorem :: JORDAN19:27

for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p in North_Arc C holds
not p in South_Arc C