let C be Simple_closed_curve; for n being Element of NAT holds (LMP C) `2 > (LMP (L~ (Cage C,n))) `2
let n be Element of 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:56;
A2:
LMP (L~ (Cage C,n)) in L~ (Cage C,n)
by JORDAN21:44;
A3:
LMP C = |[((LMP C) `1 ),((LMP C) `2 )]|
by EUCLID:57;
A4:
LMP (L~ (Cage C,n)) = |[((LMP (L~ (Cage C,n))) `1 ),((LMP (L~ (Cage C,n))) `2 )]|
by EUCLID:57;
A5:
C misses L~ (Cage C,n)
by JORDAN10:5;
A6:
LMP C in C
by JORDAN21:44;
A7:
((W-bound C) + (E-bound C)) / 2 = ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
by JORDAN1G:41;
then A8:
(LMP (L~ (Cage C,n))) `1 = ((W-bound C) + (E-bound C)) / 2
by EUCLID:56;
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 = inf (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))))
by A7, EUCLID:56;
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
set 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 14;
A18:
x `1 = ((W-bound C) + (E-bound C)) / 2
by A8, A16, TOPREAL1:def 14;
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 29;
then
x `2 in proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)))
by A19, FUNCT_2:43;
then A20:
x `2 >= (LMP (L~ (Cage C,n))) `2
by A12, A11, SEQ_4:def 5;
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:11;
hence
contradiction
by A17, A20, XXREAL_0:1;
verum
end;
(south_halfline (LMP (L~ (Cage C,n)))) \ {(LMP (L~ (Cage C,n)))} is
connected
by JORDAN1:9, 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 14;
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:131;
then A26:
not
(south_halfline (LMP (L~ (Cage C,n)))) \ {(LMP (L~ (Cage C,n)))} is
Bounded
by JORDAN21:1, TOPREAL6:99;
BDD (L~ (Cage C,n)) is
Bounded
by JORDAN2C:114;
then
LMP C in UBD (L~ (Cage C,n))
by A21, A26, A24, JORDAN2C:16;
hence
contradiction
by A6, A22, A25, XBOOLE_0:3;
verum end;