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

Upper_Arc C is_an_arc_of W-min C, E-max C by Th50;

hence Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A2, A3, Th49; :: thesis: verum

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;

Upper_Arc C is_an_arc_of W-min C, E-max C by Th50;

hence Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A2, A3, Th49; :: thesis: verum