let C be Simple_closed_curve; :: thesis: (Lower_Middle_Point C) `2 <> (Upper_Middle_Point C) `2
set l = Lower_Middle_Point C;
set u = Upper_Middle_Point C;
set w = ((W-bound C) + (E-bound C)) / 2;
assume A1: (Lower_Middle_Point C) `2 = (Upper_Middle_Point C) `2 ; :: thesis: contradiction
A2: ( (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 & (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 ) by JORDAN6:79, JORDAN6:80;
then Lower_Middle_Point C = Upper_Middle_Point C by A1, TOPREAL3:11;
then ( Lower_Middle_Point C in Lower_Arc C & Lower_Middle_Point C in Upper_Arc C ) by JORDAN6:81, JORDAN6:82;
then Lower_Middle_Point C in (Lower_Arc C) /\ (Upper_Arc C) by XBOOLE_0:def 4;
then Lower_Middle_Point C in {(W-min C),(E-max C)} by JORDAN6:def 9;
then ( Lower_Middle_Point C = W-min C or Lower_Middle_Point C = E-max C ) by TARSKI:def 2;
then ( W-bound C = ((W-bound C) + (E-bound C)) / 2 or E-bound C = ((W-bound C) + (E-bound C)) / 2 ) by A2, EUCLID:56;
hence contradiction by SPRECT_1:33; :: thesis: verum