theorem :: JORDAN6:70

for C being Simple_closed_curve
for r being Real st W-bound C <= r & r <= E-bound C holds
LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C