let C be Simple_closed_curve; (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2
set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2);
set p = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));
A1:
Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
by Th62;
Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed
by Th6;
then A2:
(Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed
by TOPS_1:8;
Lower_Arc C is_an_arc_of W-min C, E-max C
by Th50;
then
First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))
by A1, A2, JORDAN5C:def 1;
then
First_Point ((Lower_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)
by XBOOLE_0:def 4;
hence
(Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2
by Th31; verum