let C be Simple_closed_curve; :: thesis: W-bound C = W-bound (North_Arc C)
A1: W-min C in North_Arc C by Th29;
North_Arc C c= C by Th35;
hence W-bound C = W-bound (North_Arc C) by A1, JORDAN1J:65; :: thesis: verum