theorem Th18: :: JORDAN21:18

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