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;
A1: (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by JORDAN6:64;
A2: (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by JORDAN6:65;
assume (Lower_Middle_Point C) `2 = (Upper_Middle_Point C) `2 ; :: thesis: contradiction
then Lower_Middle_Point C = Upper_Middle_Point C by A1, A2, TOPREAL3:6;
then ( Lower_Middle_Point C in Lower_Arc C & Lower_Middle_Point C in Upper_Arc C ) by JORDAN6:66, JORDAN6:67;
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 A1, EUCLID:52;
hence contradiction by SPRECT_1:31; :: thesis: verum