let C be Simple_closed_curve; (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 = upper_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) & (LMP C) `2 = lower_bound (proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) )
by EUCLID:52;
set u = Upper_Middle_Point C;
set l = Lower_Middle_Point C;
A2:
(Lower_Middle_Point C) `2 = proj2 . (Lower_Middle_Point C)
by PSCOMP_1:def 6;
(Lower_Middle_Point C) `1 = ((E-bound C) + (W-bound C)) / 2
by JORDAN6:64;
then A3:
Lower_Middle_Point C in Vertical_Line (((E-bound C) + (W-bound C)) / 2)
by JORDAN6:31;
Lower_Middle_Point C in C
by Th14;
then
Lower_Middle_Point C in C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))
by A3, XBOOLE_0:def 4;
then A4:
(Lower_Middle_Point C) `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))
by A2, FUNCT_2:35;
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is bounded
by TOPREAL6:89;
then A5:
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is real-bounded
by JCT_MISC:14;
(Upper_Middle_Point C) `1 = ((E-bound C) + (W-bound C)) / 2
by JORDAN6:65;
then
( Upper_Middle_Point C in C & Upper_Middle_Point C in Vertical_Line (((E-bound C) + (W-bound C)) / 2) )
by JORDAN6:31, JORDAN6:68;
then A6:
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 6;
then A7:
(Upper_Middle_Point C) `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))
by A6, FUNCT_2:35;
(Upper_Middle_Point C) `2 <> (Lower_Middle_Point C) `2
by Th15;
hence
(LMP C) `2 < (UMP C) `2
by A1, A5, A7, A4, SEQ_4:12; verum