let C be Simple_closed_curve; for n being Nat holds (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2
let n be 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:52;
A2:
UMP (L~ (Cage (C,n))) in L~ (Cage (C,n))
by JORDAN21:30;
A3:
UMP C = |[((UMP C) `1),((UMP C) `2)]|
by EUCLID:53;
A4:
UMP (L~ (Cage (C,n))) = |[((UMP (L~ (Cage (C,n)))) `1),((UMP (L~ (Cage (C,n)))) `2)]|
by EUCLID:53;
A5:
C misses L~ (Cage (C,n))
by JORDAN10:5;
A6:
UMP C in C
by JORDAN21:30;
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:
(UMP (L~ (Cage (C,n)))) `1 = ((W-bound C) + (E-bound C)) / 2
by EUCLID:52;
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 = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))))
by A7, EUCLID:52;
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
object 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 10;
A18:
x `1 = ((W-bound C) + (E-bound C)) / 2
by A8, A16, TOPREAL1:def 10;
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 <= (UMP (L~ (Cage (C,n)))) `2
by A12, A11, SEQ_4:def 1;
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:6;
hence
contradiction
by A17, A20, XXREAL_0:1;
verum
end;
(north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} is
convex
by 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 10;
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:122;
then A26:
not
(north_halfline (UMP (L~ (Cage (C,n))))) \ {(UMP (L~ (Cage (C,n))))} is
bounded
by JORDAN21:1, TOPREAL6:90;
BDD (L~ (Cage (C,n))) is
bounded
by JORDAN2C:106;
then
UMP C in UBD (L~ (Cage (C,n)))
by A21, A26, A24, RLTOPSP1:42;
hence
contradiction
by A6, A22, A25, XBOOLE_0:3;
verum end;