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