let C be Simple_closed_curve; :: thesis: (LMP C) `2 < (UMP C) `2
set w = ((E-bound C) + (W-bound C)) / 2;
set X = C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2));
A1: ( (UMP C) `2 = sup (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & (LMP C) `2 = inf (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) ) by EUCLID:56;
C is Bounded by JORDAN2C:73;
then C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Bounded by TOPREAL6:98;
then A2: proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded by JCT_MISC:23;
set u = Upper_Middle_Point C;
set l = Lower_Middle_Point C;
A3: (Upper_Middle_Point C) `2 <> (Lower_Middle_Point C) `2 by Th24;
(Upper_Middle_Point C) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN6:80;
then ( Upper_Middle_Point C in C & Upper_Middle_Point C in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ) by JORDAN6:34, JORDAN6:83;
then A4: Upper_Middle_Point C in C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by XBOOLE_0:def 4;
(Upper_Middle_Point C) `2 = proj2 . (Upper_Middle_Point C) by PSCOMP_1:def 29;
then A5: (Upper_Middle_Point C) `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A4, FUNCT_2:43;
(Lower_Middle_Point C) `1 = ((E-bound C) + (W-bound C)) / 2 by JORDAN6:79;
then ( Lower_Middle_Point C in C & Lower_Middle_Point C in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ) by Th23, JORDAN6:34;
then A6: Lower_Middle_Point C in C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by XBOOLE_0:def 4;
(Lower_Middle_Point C) `2 = proj2 . (Lower_Middle_Point C) by PSCOMP_1:def 29;
then (Lower_Middle_Point C) `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A6, FUNCT_2:43;
hence (LMP C) `2 < (UMP C) `2 by A1, A2, A3, A5, SEQ_4:25; :: thesis: verum