:: deftheorem Def1 defines with_the_max_arc JORDAN21:def 1 :
for D being Subset of (TOP-REAL 2) holds
( D is with_the_max_arc iff D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2) );