let C be Simple_closed_curve; :: thesis: Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
A1: W-bound C <= E-bound C by SPRECT_1:21;
(W-min C) `1 = W-bound C by EUCLID:52;
then A2: (W-min C) `1 <= ((W-bound C) + (E-bound C)) / 2 by A1, Th1;
(E-max C) `1 = E-bound C by EUCLID:52;
then A3: ((W-bound C) + (E-bound C)) / 2 <= (E-max C) `1 by A1, Th1;
Lower_Arc C is_an_arc_of W-min C, E-max C by Th50;
hence Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A2, A3, Th49; :: thesis: verum