let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in C holds
north_halfline p meets L~ (Cage (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st p in C holds
north_halfline p meets L~ (Cage (C,n))
let p be Point of (TOP-REAL 2); ( p in C implies north_halfline p meets L~ (Cage (C,n)) )
set f = Cage (C,n);
assume A1:
p in C
; north_halfline p meets L~ (Cage (C,n))
set X = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } ;
A2:
{ q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } = north_halfline p
by TOPREAL1:30;
(max ((N-bound (L~ (Cage (C,n)))),(p `2))) + 1 > (N-bound (L~ (Cage (C,n)))) + 0
by XREAL_1:8, XXREAL_0:25;
then
( (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) & |[(p `1),((max ((N-bound (L~ (Cage (C,n)))),(p `2))) + 1)]| `2 > N-bound (L~ (Cage (C,n))) )
by EUCLID:52, JORDAN9:32;
then
|[(p `1),((max ((N-bound (L~ (Cage (C,n)))),(p `2))) + 1)]| in LeftComp (Cage (C,n))
by JORDAN2C:113;
then A3:
|[(p `1),((max ((N-bound (L~ (Cage (C,n)))),(p `2))) + 1)]| in UBD (L~ (Cage (C,n)))
by GOBRD14:36;
LeftComp (Cage (C,n)) is_outside_component_of L~ (Cage (C,n))
by GOBRD14:34;
then
LeftComp (Cage (C,n)) is_a_component_of (L~ (Cage (C,n))) `
by JORDAN2C:def 3;
then A4:
UBD (L~ (Cage (C,n))) is_a_component_of (L~ (Cage (C,n))) `
by GOBRD14:36;
reconsider X = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } as connected Subset of (TOP-REAL 2) by A2;
A5:
( C c= BDD (L~ (Cage (C,n))) & p in X )
by JORDAN10:12;
max ((N-bound (L~ (Cage (C,n)))),(p `2)) >= p `2
by XXREAL_0:25;
then
(max ((N-bound (L~ (Cage (C,n)))),(p `2))) + 1 >= (p `2) + 0
by XREAL_1:7;
then A6:
|[(p `1),((max ((N-bound (L~ (Cage (C,n)))),(p `2))) + 1)]| `2 >= p `2
by EUCLID:52;
|[(p `1),((max ((N-bound (L~ (Cage (C,n)))),(p `2))) + 1)]| `1 = p `1
by EUCLID:52;
then
|[(p `1),((max ((N-bound (L~ (Cage (C,n)))),(p `2))) + 1)]| in X
by A6;
then A7:
X meets UBD (L~ (Cage (C,n)))
by A3, XBOOLE_0:3;
assume
not north_halfline p meets L~ (Cage (C,n))
; contradiction
then
X c= (L~ (Cage (C,n))) `
by A2, SUBSET_1:23;
then
X c= UBD (L~ (Cage (C,n)))
by A7, A4, GOBOARD9:4;
then
p in (BDD (L~ (Cage (C,n)))) /\ (UBD (L~ (Cage (C,n))))
by A1, A5, XBOOLE_0:def 4;
then
BDD (L~ (Cage (C,n))) meets UBD (L~ (Cage (C,n)))
;
hence
contradiction
by JORDAN2C:24; verum