let A be Subset of (TOP-REAL 2); ( A is vertical & not A is empty & A is compact implies A is with_the_max_arc )
assume A1:
( A is vertical & not A is empty & A is compact )
; A is with_the_max_arc
then A2:
W-bound A = E-bound A
by SPRECT_1:15;
A3:
E-min A in A
by A1, SPRECT_1:14;
(E-min A) `1 = E-bound A
by EUCLID:52;
then
E-min A in Vertical_Line (((W-bound A) + (E-bound A)) / 2)
by A2, JORDAN6:31;
hence
A meets Vertical_Line (((W-bound A) + (E-bound A)) / 2)
by A3, XBOOLE_0:3; JORDAN21:def 1 verum