let C be Simple_closed_curve; :: thesis: C is with_the_max_arc
A1: Upper_Middle_Point C in C by JORDAN6:83;
(Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by JORDAN6:80;
then Upper_Middle_Point C in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN6:34;
hence C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A1, XBOOLE_0:3; :: according to JORDAN21:def 1 :: thesis: verum