theorem Th17: :: JORDAN21:17

for C being Simple_closed_curve holds W-bound C = W-bound (Upper_Arc C)