theorem :: JORDAN21:47

for C being Simple_closed_curve holds (UMP (Upper_Arc C)) `2 <= N-bound C