theorem Th21: :: JORDAN21:21

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