theorem Th63: :: JORDAN6:63

for C being Simple_closed_curve holds Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)