theorem :: JORDAN6:64

for C being Simple_closed_curve holds (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2