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:56;
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 29;
(Lower_Middle_Point C) `1 = ((E-bound C) + (W-bound C)) / 2
by JORDAN6:79;
then A3:
Lower_Middle_Point C in Vertical_Line (((E-bound C) + (W-bound C)) / 2)
by JORDAN6:34;
Lower_Middle_Point C in C
by Th23;
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:43;
C is Bounded
by JORDAN2C:73;
then
C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) is Bounded
by TOPREAL6:98;
then A5:
proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded
by JCT_MISC:23;
(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 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 29;
then A7:
(Upper_Middle_Point C) `2 in proj2 .: (C /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))
by A6, FUNCT_2:43;
(Upper_Middle_Point C) `2 <> (Lower_Middle_Point C) `2
by Th24;
hence
(LMP C) `2 < (UMP C) `2
by A1, A5, A7, A4, SEQ_4:25; verum