theorem Th22: :: JORDAN21:22

for C being Simple_closed_curve holds
( 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 )