let C be Simple_closed_curve; :: thesis: W-bound C = W-bound (South_Arc C)
A1: W-min C in South_Arc C by Th31;
South_Arc C c= C by Th36;
hence W-bound C = W-bound (South_Arc C) by A1, JORDAN1J:65; :: thesis: verum