:: deftheorem defines Lower_Middle_Point JORDAN6:def 11 :
for C being Simple_closed_curve holds Lower_Middle_Point C = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));