let C be Simple_closed_curve; for n being Element of NAT holds (UMP C) `2 < (UMP (L~ (Cage C,n))) `2
let n be Element of NAT ; (UMP C) `2 < (UMP (L~ (Cage C,n))) `2
set p = UMP (L~ (Cage C,n));
set u = UMP C;
set w = ((W-bound C) + (E-bound C)) / 2;
A1:
(UMP C) `1 = ((W-bound C) + (E-bound C)) / 2
by EUCLID:56;
A2:
UMP (L~ (Cage C,n)) in L~ (Cage C,n)
by JORDAN21:43;
A3:
UMP C = |[((UMP C) `1 ),((UMP C) `2 )]|
by EUCLID:57;
A4:
UMP (L~ (Cage C,n)) = |[((UMP (L~ (Cage C,n))) `1 ),((UMP (L~ (Cage C,n))) `2 )]|
by EUCLID:57;
A5:
C misses L~ (Cage C,n)
by JORDAN10:5;
A6:
UMP C in C
by JORDAN21:43;
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:
(UMP (L~ (Cage C,n))) `1 = ((W-bound C) + (E-bound C)) / 2
by EUCLID:56;
assume A9:
not (UMP C) `2 < (UMP (L~ (Cage C,n))) `2
; contradiction
per cases
( (UMP C) `2 = (UMP (L~ (Cage C,n))) `2 or (UMP C) `2 > (UMP (L~ (Cage C,n))) `2 )
by A9, XXREAL_0:1;
suppose A10:
(UMP C) `2 > (UMP (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_above )
by A7, JORDAN21:12, JORDAN21:13;
A12:
(UMP (L~ (Cage C,n))) `2 = sup (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))))
by A7, EUCLID:56;
A13:
(north_halfline (UMP (L~ (Cage C,n)))) \ {(UMP (L~ (Cage C,n)))} misses L~ (Cage C,n)
proof
assume
(north_halfline (UMP (L~ (Cage C,n)))) \ {(UMP (L~ (Cage C,n)))} meets L~ (Cage C,n)
;
contradiction
then consider x being
set such that A14:
x in (north_halfline (UMP (L~ (Cage C,n)))) \ {(UMP (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 north_halfline (UMP (L~ (Cage C,n)))
by A14, XBOOLE_0:def 5;
then A17:
x `2 >= (UMP (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 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 <= (UMP (L~ (Cage C,n))) `2
by A12, A11, SEQ_4:def 4;
not
x in {(UMP (L~ (Cage C,n)))}
by A14, XBOOLE_0:def 5;
then
x <> UMP (L~ (Cage C,n))
by TARSKI:def 1;
then
x `2 <> (UMP (L~ (Cage C,n))) `2
by A8, A18, TOPREAL3:11;
hence
contradiction
by A17, A20, XXREAL_0:1;
verum
end;
(north_halfline (UMP (L~ (Cage C,n)))) \ {(UMP (L~ (Cage C,n)))} is
connected
by JORDAN1:9, JORDAN21:6;
then A21:
(
(north_halfline (UMP (L~ (Cage C,n)))) \ {(UMP (L~ (Cage C,n)))} c= UBD (L~ (Cage C,n)) or
(north_halfline (UMP (L~ (Cage C,n)))) \ {(UMP (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
UMP C in {(UMP (L~ (Cage C,n)))}
by A10, TARSKI:def 1;
UMP C in north_halfline (UMP (L~ (Cage C,n)))
by A1, A8, A10, TOPREAL1:def 12;
then A24:
UMP C in (north_halfline (UMP (L~ (Cage C,n)))) \ {(UMP (L~ (Cage C,n)))}
by A23, XBOOLE_0:def 5;
A25:
UBD C misses C
by JORDAN21:10;
not
north_halfline (UMP (L~ (Cage C,n))) is
Bounded
by JORDAN2C:130;
then A26:
not
(north_halfline (UMP (L~ (Cage C,n)))) \ {(UMP (L~ (Cage C,n)))} is
Bounded
by JORDAN21:1, TOPREAL6:99;
BDD (L~ (Cage C,n)) is
Bounded
by JORDAN2C:114;
then
UMP C in UBD (L~ (Cage C,n))
by A21, A26, A24, JORDAN2C:16;
hence
contradiction
by A6, A22, A25, XBOOLE_0:3;
verum end;