let n be 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
east_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
east_halfline p meets L~ (Cage (C,n))
let p be Point of (TOP-REAL 2); :: thesis: ( p in C implies east_halfline p meets L~ (Cage (C,n)) )
set f = Cage (C,n);
assume A1: p in C ; :: thesis: east_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 ) } = east_halfline p by TOPREAL1:32;
(max ((E-bound (L~ (Cage (C,n)))),(p `1))) + 1 > (E-bound (L~ (Cage (C,n)))) + 0 by XREAL_1:8, XXREAL_0:25;
then ( (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) & |[((max ((E-bound (L~ (Cage (C,n)))),(p `1))) + 1),(p `2)]| `1 > E-bound (L~ (Cage (C,n))) ) by EUCLID:52, JORDAN9:32;
then |[((max ((E-bound (L~ (Cage (C,n)))),(p `1))) + 1),(p `2)]| in LeftComp (Cage (C,n)) by JORDAN2C:111;
then A3: |[((max ((E-bound (L~ (Cage (C,n)))),(p `1))) + 1),(p `2)]| 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 ((E-bound (L~ (Cage (C,n)))),(p `1)) >= p `1 by XXREAL_0:25;
then (max ((E-bound (L~ (Cage (C,n)))),(p `1))) + 1 >= (p `1) + 0 by XREAL_1:7;
then A6: |[((max ((E-bound (L~ (Cage (C,n)))),(p `1))) + 1),(p `2)]| `1 >= p `1 by EUCLID:52;
|[((max ((E-bound (L~ (Cage (C,n)))),(p `1))) + 1),(p `2)]| `2 = p `2 by EUCLID:52;
then |[((max ((E-bound (L~ (Cage (C,n)))),(p `1))) + 1),(p `2)]| in X by A6;
then A7: X meets UBD (L~ (Cage (C,n))) by A3, XBOOLE_0:3;
assume not east_halfline p meets L~ (Cage (C,n)) ; :: thesis: 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; :: thesis: verum