let C be Simple_closed_curve; 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; ( 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
; (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
; 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))
;
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;
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; verum