let C be Simple_closed_curve; ( not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )
set w = ((W-bound C) + (E-bound C)) / 2;
A1:
W-bound C < E-bound C
by SPRECT_1:31;
(E-max C) `1 = E-bound C
by EUCLID:52;
then A2:
((W-bound C) + (E-bound C)) / 2 <= (E-max C) `1
by A1, XREAL_1:226;
Lower_Arc C is_an_arc_of E-max C, W-min C
by JORDAN6:def 9;
then A3:
Lower_Arc C is_an_arc_of W-min C, E-max C
by JORDAN5B:14;
(W-min C) `1 = W-bound C
by EUCLID:52;
then
(W-min C) `1 <= ((W-bound C) + (E-bound C)) / 2
by A1, XREAL_1:226;
then
Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
by A3, A2, JORDAN6:49;
then
not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty
;
hence
( not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )
by Lm1, RELAT_1:119; verum