let C be Simple_closed_curve; :: thesis: Upper_Middle_Point C in C
A1: Upper_Middle_Point C in Upper_Arc C by Th67;
Upper_Arc C c= C by Th61;
hence Upper_Middle_Point C in C by A1; :: thesis: verum