let C be Simple_closed_curve; for n being Nat holds (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2
let n be Nat; (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2
set p = LMP (L~ (Cage (C,n)));
set u = LMP C;
set w = ((W-bound C) + (E-bound C)) / 2;
A1:
(LMP C) `1 = ((W-bound C) + (E-bound C)) / 2
by EUCLID:52;
A2:
LMP (L~ (Cage (C,n))) in L~ (Cage (C,n))
by JORDAN21:31;
A3:
LMP C = |[((LMP C) `1),((LMP C) `2)]|
by EUCLID:53;
A4:
LMP (L~ (Cage (C,n))) = |[((LMP (L~ (Cage (C,n)))) `1),((LMP (L~ (Cage (C,n)))) `2)]|
by EUCLID:53;
A5:
C misses L~ (Cage (C,n))
by JORDAN10:5;
A6:
LMP C in C
by JORDAN21:31;
A7:
((W-bound C) + (E-bound C)) / 2 = ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
by JORDAN1G:33;
then A8:
(LMP (L~ (Cage (C,n)))) `1 = ((W-bound C) + (E-bound C)) / 2
by EUCLID:52;
assume A9:
not (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2
; contradiction
per cases
( (LMP C) `2 = (LMP (L~ (Cage (C,n)))) `2 or (LMP C) `2 < (LMP (L~ (Cage (C,n)))) `2 )
by A9, XXREAL_0:1;
suppose A10:
(LMP C) `2 < (LMP (L~ (Cage (C,n)))) `2
;
contradictionA11:
( not
proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is
empty &
proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is
bounded_below )
by A7, JORDAN21:12, JORDAN21:13;
A12:
(LMP (L~ (Cage (C,n)))) `2 = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))))
by A7, EUCLID:52;
A13:
(south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} misses L~ (Cage (C,n))
proof
assume
(south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} meets L~ (Cage (C,n))
;
contradiction
then consider x being
object such that A14:
x in (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))}
and A15:
x in L~ (Cage (C,n))
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A15;
A16:
x in south_halfline (LMP (L~ (Cage (C,n))))
by A14, XBOOLE_0:def 5;
then A17:
x `2 <= (LMP (L~ (Cage (C,n)))) `2
by TOPREAL1:def 12;
A18:
x `1 = ((W-bound C) + (E-bound C)) / 2
by A8, A16, TOPREAL1:def 12;
then
x in Vertical_Line (((W-bound C) + (E-bound C)) / 2)
;
then A19:
x in (L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))
by A15, XBOOLE_0:def 4;
proj2 . x = x `2
by PSCOMP_1:def 6;
then
x `2 in proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))
by A19, FUNCT_2:35;
then A20:
x `2 >= (LMP (L~ (Cage (C,n)))) `2
by A12, A11, SEQ_4:def 2;
not
x in {(LMP (L~ (Cage (C,n))))}
by A14, XBOOLE_0:def 5;
then
x <> LMP (L~ (Cage (C,n)))
by TARSKI:def 1;
then
x `2 <> (LMP (L~ (Cage (C,n)))) `2
by A8, A18, TOPREAL3:6;
hence
contradiction
by A17, A20, XXREAL_0:1;
verum
end;
(south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} is
convex
by JORDAN21:7;
then A21:
(
(south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} c= UBD (L~ (Cage (C,n))) or
(south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} c= BDD (L~ (Cage (C,n))) )
by A13, JORDAN1K:19;
A22:
UBD (L~ (Cage (C,n))) c= UBD C
by JORDAN10:13;
A23:
not
LMP C in {(LMP (L~ (Cage (C,n))))}
by A10, TARSKI:def 1;
LMP C in south_halfline (LMP (L~ (Cage (C,n))))
by A1, A8, A10, TOPREAL1:def 12;
then A24:
LMP C in (south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))}
by A23, XBOOLE_0:def 5;
A25:
UBD C misses C
by JORDAN21:10;
not
south_halfline (LMP (L~ (Cage (C,n)))) is
bounded
by JORDAN2C:123;
then A26:
not
(south_halfline (LMP (L~ (Cage (C,n))))) \ {(LMP (L~ (Cage (C,n))))} is
bounded
by JORDAN21:1, TOPREAL6:90;
BDD (L~ (Cage (C,n))) is
bounded
by JORDAN2C:106;
then
LMP C in UBD (L~ (Cage (C,n)))
by A21, A26, A24, RLTOPSP1:42;
hence
contradiction
by A6, A22, A25, XBOOLE_0:3;
verum end;