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
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:39;
(max (E-bound (L~ (Cage C,n))),(p `1 )) + 1 > (E-bound (L~ (Cage C,n))) + 0 by XREAL_1:10, 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:56, JORDAN9:34;
then |[((max (E-bound (L~ (Cage C,n))),(p `1 )) + 1),(p `2 )]| in LeftComp (Cage C,n) by JORDAN2C:119;
then A3: |[((max (E-bound (L~ (Cage C,n))),(p `1 )) + 1),(p `2 )]| 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 (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:9;
then A6: |[((max (E-bound (L~ (Cage C,n))),(p `1 )) + 1),(p `2 )]| `1 >= p `1 by EUCLID:56;
|[((max (E-bound (L~ (Cage C,n))),(p `1 )) + 1),(p `2 )]| `2 = p `2 by EUCLID:56;
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: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