let C be Simple_closed_curve; :: thesis: for i, j being Element of NAT st i <= j holds
(UMP (L~ (Cage C,j))) `2 <= (UMP (L~ (Cage C,i))) `2
let i, j be Element of 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:55;
A2: (W-bound (L~ (Cage C,j))) + (E-bound (L~ (Cage C,j))) = (W-bound C) + (E-bound C) by JORDAN1G:41;
then A3: (UMP (L~ (Cage C,j))) `2 = sup (proj2 .: ((L~ (Cage C,j)) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:56;
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:52;
A5: (W-bound (L~ (Cage C,i))) + (E-bound (L~ (Cage C,i))) = (W-bound C) + (E-bound C) by JORDAN1G:41;
then A6: (UMP (L~ (Cage C,i))) `2 = sup (proj2 .: ((L~ (Cage C,i)) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2)))) by EUCLID:56;
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 number such that
A8: r in proj2 .: ((L~ (Cage C,j)) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) and
A9: (sup (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 4;
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 29;
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 set 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 12
.= ((E-bound C) + (W-bound C)) / 2 by A13, JORDAN6:34 ;
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 29;
then y `2 in proj2 .: ((L~ (Cage C,i)) /\ (Vertical_Line (((E-bound C) + (W-bound C)) / 2))) by A16, FUNCT_2:43;
then A17: y `2 <= (UMP (L~ (Cage C,i))) `2 by A6, A7, SEQ_4:def 4;
y `2 >= x `2 by A14, TOPREAL1:def 12;
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:137;
x in north_halfline x by TOPREAL1:45;
then x in UBD (L~ (Cage C,i)) by A18;
then A19: x in LeftComp (Cage C,i) by GOBRD14:46;
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:43; :: thesis: verum