theorem
Th63
:
:: JORDAN6:63
for
C
being
Simple_closed_curve
holds
Upper_Arc
C
meets
Vertical_Line
(
(
(
W-bound
C
)
+
(
E-bound
C
)
)
/
2
)