( W-bound C = W-bound (Upper_Arc C) & E-bound C = E-bound (Upper_Arc C) ) by Th17, Th18;
hence Upper_Arc C meets Vertical_Line (((W-bound (Upper_Arc C)) + (E-bound (Upper_Arc C))) / 2) by JORDAN6:63; :: according to JORDAN21:def 1 :: thesis: verum