let C be Simple_closed_curve; :: thesis: for i, j being Nat st i <= j holds
(UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2
let i, j be Nat; :: thesis: ( i <= j implies (UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2 )
set w = ((E-bound C) + (W-bound C)) / 2;
set ui = UMP (L~ (Cage (C,i)));
set uj = UMP (L~ (Cage (C,j)));
assume i <= j ; :: thesis: (UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2
then A1: LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j)) by JORDAN1H:47;
A2: (W-bound (L~ (Cage (C,j)))) + (E-bound (L~ (Cage (C,j)))) = (W-bound C) + (E-bound C) by JORDAN1G:33;
then A3: (UMP (L~ (Cage (C,j)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
assume (UMP (L~ (Cage (C,j)))) `2 > (UMP (L~ (Cage (C,i)))) `2 ; :: thesis: contradiction
then A4: ((UMP (L~ (Cage (C,j)))) `2) - ((UMP (L~ (Cage (C,i)))) `2) > 0 by XREAL_1:50;
A5: (W-bound (L~ (Cage (C,i)))) + (E-bound (L~ (Cage (C,i)))) = (W-bound C) + (E-bound C) by JORDAN1G:33;
then A6: (UMP (L~ (Cage (C,i)))) `2 = upper_bound (proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:52;
A7: ( not proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above ) by A5, JORDAN21:12, JORDAN21:13;
( not proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is empty & proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) is bounded_above ) by A2, JORDAN21:12, JORDAN21:13;
then consider r being Real such that
A8: r in proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) and
A9: (upper_bound (proj2 .: ((L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))))) - (((UMP (L~ (Cage (C,j)))) `2) - ((UMP (L~ (Cage (C,i)))) `2)) < r by A4, SEQ_4:def 1;
consider x being Point of (TOP-REAL 2) such that
A10: x in (L~ (Cage (C,j))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) and
A11: proj2 . x = r by A8, Lm1;
A12: x `2 = r by A11, PSCOMP_1:def 6;
north_halfline x misses L~ (Cage (C,i))

proof

A13: x in Vertical_Line (((E-bound C) + (W-bound C)) / 2) by A10, XBOOLE_0:def 4;
assume north_halfline x meets L~ (Cage (C,i)) ; :: thesis: contradiction
then consider y being object such that
A14: y in north_halfline x and
A15: y in L~ (Cage (C,i)) by XBOOLE_0:3;
reconsider y = y as Point of (TOP-REAL 2) by A15;
y `1 = x `1 by A14, TOPREAL1:def 10
.= ((E-bound C) + (W-bound C)) / 2 by A13, JORDAN6:31 ;
then y in Vertical_Line (((E-bound C) + (W-bound C)) / 2) ;
then A16: y in (L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)) by A15, XBOOLE_0:def 4;
proj2 . y = y `2 by PSCOMP_1:def 6;
then y `2 in proj2 .: ((L~ (Cage (C,i))) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A16, FUNCT_2:35;
then A17: y `2 <= (UMP (L~ (Cage (C,i)))) `2 by A6, A7, SEQ_4:def 1;
y `2 >= x `2 by A14, TOPREAL1:def 10;
hence contradiction by A3, A9, A12, A17, XXREAL_0:2; :: thesis: verum

end;

then A18: north_halfline x c= UBD (L~ (Cage (C,i))) by JORDAN2C:129;
x in north_halfline x by TOPREAL1:38;
then x in UBD (L~ (Cage (C,i))) by A18;
then A19: x in LeftComp (Cage (C,i)) by GOBRD14:36;
x in L~ (Cage (C,j)) by A10, XBOOLE_0:def 4;
then LeftComp (Cage (C,j)) meets L~ (Cage (C,j)) by A1, A19, XBOOLE_0:3;
hence contradiction by SPRECT_3:26; :: thesis: verum