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