let C be Simple_closed_curve; Upper_Middle_Point C in Upper_Arc C
set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2);
set p = First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
A1:
Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
by Th63;
Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed
by Th6;
then A2:
(Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed
by TOPS_1:8;
A3:
Upper_Arc C is_an_arc_of E-max C, W-min C
by Th50;
then
First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) = Last_Point ((Upper_Arc C),(E-max C),(W-min C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)))
by A1, A2, JORDAN5C:18;
then
First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) /\ (Upper_Arc C)
by A1, A2, A3, JORDAN5C:def 2;
hence
Upper_Middle_Point C in Upper_Arc C
by XBOOLE_0:def 4; verum