theorem :: JORDAN6:66

for C being Simple_closed_curve holds Lower_Middle_Point C in Lower_Arc C