theorem :: JORDAN22:39

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