let C be Simple_closed_curve; ( not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Upper_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;
(W-min C) `1 = W-bound C
by EUCLID:52;
then
( Upper_Arc C is_an_arc_of W-min C, E-max C & (W-min C) `1 <= ((W-bound C) + (E-bound C)) / 2 )
by A1, JORDAN6:def 8, XREAL_1:226;
then
Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
by A2, JORDAN6:49;
then
not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty
;
hence
( not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )
by Lm1, RELAT_1:119; verum