let D be Subset of (TOP-REAL 2); :: thesis: ( D is with_the_max_arc implies not D is empty )
assume D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2) ; :: according to JORDAN21:def 1 :: thesis: not D is empty
hence not D is empty ; :: thesis: verum