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