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