let n be Element of NAT ; :: thesis: 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); :: thesis: 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); :: thesis: ( p in C implies north_halfline p meets L~ (Cage C,n) )
set f = Cage C,n;
assume A1: p in C ; :: thesis: 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:37;
(max (N-bound (L~ (Cage C,n))),(p `2 )) + 1 > (N-bound (L~ (Cage C,n))) + 0 by XREAL_1:10, 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:56, JORDAN9:34;
then |[(p `1 ),((max (N-bound (L~ (Cage C,n))),(p `2 )) + 1)]| in LeftComp (Cage C,n) by JORDAN2C:121;
then A3: |[(p `1 ),((max (N-bound (L~ (Cage C,n))),(p `2 )) + 1)]| in UBD (L~ (Cage C,n)) by GOBRD14:46;
LeftComp (Cage C,n) is_outside_component_of L~ (Cage C,n) by GOBRD14:44;
then LeftComp (Cage C,n) is_a_component_of (L~ (Cage C,n)) ` by JORDAN2C:def 4;
then A4: UBD (L~ (Cage C,n)) is_a_component_of (L~ (Cage C,n)) ` by GOBRD14:46;
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:9;
then A6: |[(p `1 ),((max (N-bound (L~ (Cage C,n))),(p `2 )) + 1)]| `2 >= p `2 by EUCLID:56;
|[(p `1 ),((max (N-bound (L~ (Cage C,n))),(p `2 )) + 1)]| `1 = p `1 by EUCLID:56;
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) ; :: thesis: contradiction
then X c= (L~ (Cage C,n)) ` by A2, SUBSET_1:43;
then X c= UBD (L~ (Cage C,n)) by A7, A4, GOBOARD9:6;
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)) by XBOOLE_0:4;
hence contradiction by JORDAN2C:28; :: thesis: verum