theorem :: JORDAN22:41

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