let C be Simple_closed_curve; :: thesis: for n being Element of NAT holds (LMP C) `2 > (LMP (L~ (Cage C,n))) `2
let n be Element of NAT ; :: thesis: (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;
assume A1:
not (LMP C) `2 > (LMP (L~ (Cage C,n))) `2
; :: thesis: contradiction
A2:
(LMP C) `1 = ((W-bound C) + (E-bound C)) / 2
by EUCLID:56;
A3:
((W-bound C) + (E-bound C)) / 2 = ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
by JORDAN1G:41;
then A4:
(LMP (L~ (Cage C,n))) `1 = ((W-bound C) + (E-bound C)) / 2
by EUCLID:56;
A5:
( LMP (L~ (Cage C,n)) = |[((LMP (L~ (Cage C,n))) `1 ),((LMP (L~ (Cage C,n))) `2 )]| & LMP C = |[((LMP C) `1 ),((LMP C) `2 )]| )
by EUCLID:57;
A6:
C misses L~ (Cage C,n)
by JORDAN10:5;
A7:
LMP C in C
by JORDAN21:44;
A8:
LMP (L~ (Cage C,n)) in L~ (Cage C,n)
by JORDAN21:44;
per cases
( (LMP C) `2 = (LMP (L~ (Cage C,n))) `2 or (LMP C) `2 < (LMP (L~ (Cage C,n))) `2 )
by A1, XXREAL_0:1;
suppose A9:
(LMP C) `2 < (LMP (L~ (Cage C,n))) `2
;
:: thesis: contradictionA10:
(LMP (L~ (Cage C,n))) `2 = inf (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))))
by A3, EUCLID:56;
A11:
( 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 A3, JORDAN21:12, JORDAN21:13;
A12:
(south_halfline (LMP (L~ (Cage C,n)))) \ {(LMP (L~ (Cage C,n)))} is
connected
by JORDAN1:9, JORDAN21:7;
(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)
;
:: thesis: contradiction
then consider x being
set such that A13:
x in (south_halfline (LMP (L~ (Cage C,n)))) \ {(LMP (L~ (Cage C,n)))}
and A14:
x in L~ (Cage C,n)
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A14;
A15:
x in south_halfline (LMP (L~ (Cage C,n)))
by A13, XBOOLE_0:def 5;
then A16:
x `2 <= (LMP (L~ (Cage C,n))) `2
by TOPREAL1:def 14;
A17:
x `1 = ((W-bound C) + (E-bound C)) / 2
by A4, A15, TOPREAL1:def 14;
not
x in {(LMP (L~ (Cage C,n)))}
by A13, XBOOLE_0:def 5;
then
x <> LMP (L~ (Cage C,n))
by TARSKI:def 1;
then A18:
x `2 <> (LMP (L~ (Cage C,n))) `2
by A4, A17, TOPREAL3:11;
x in Vertical_Line (((W-bound C) + (E-bound C)) / 2)
by A17;
then A19:
x in (L~ (Cage C,n)) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))
by A14, 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
x `2 >= (LMP (L~ (Cage C,n))) `2
by A10, A11, SEQ_4:def 5;
hence
contradiction
by A16, A18, XXREAL_0:1;
:: thesis: verum
end; then A20:
(
(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 A12, JORDAN1K:19;
A21:
not
south_halfline (LMP (L~ (Cage C,n))) is
Bounded
by JORDAN2C:131;
A22:
BDD (L~ (Cage C,n)) is
Bounded
by JORDAN2C:114;
A23:
not
(south_halfline (LMP (L~ (Cage C,n)))) \ {(LMP (L~ (Cage C,n)))} is
Bounded
by A21, JORDAN21:1, TOPREAL6:99;
A24:
UBD (L~ (Cage C,n)) c= UBD C
by JORDAN10:13;
A25:
LMP C in south_halfline (LMP (L~ (Cage C,n)))
by A2, A4, A9, TOPREAL1:def 14;
not
LMP C in {(LMP (L~ (Cage C,n)))}
by A9, TARSKI:def 1;
then
LMP C in (south_halfline (LMP (L~ (Cage C,n)))) \ {(LMP (L~ (Cage C,n)))}
by A25, XBOOLE_0:def 5;
then A26:
LMP C in UBD (L~ (Cage C,n))
by A20, A22, A23, JORDAN2C:16;
UBD C misses C
by JORDAN21:10;
hence
contradiction
by A7, A24, A26, XBOOLE_0:3;
:: thesis: verum end;