for C being Simple_closed_curve holds Upper_Middle_Point C in Upper_Arc C