theorem Th20: :: JORDAN21:20

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