let C be Simple_closed_curve; :: thesis: 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; :: thesis: verum

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; :: thesis: verum