let C be Simple_closed_curve; :: thesis: E-bound C = E-bound (North_Arc C)
A1: E-max C in North_Arc C by Th32;
North_Arc C c= C by Th37;
hence E-bound C = E-bound (North_Arc C) by A1, JORDAN1J:66; :: thesis: verum