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
west_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
west_halfline p meets L~ (Cage (C,n))
let p be Point of (TOP-REAL 2); :: thesis: ( p in C implies west_halfline p meets L~ (Cage (C,n)) )
set f = Cage (C,n);
assume A1: p in C ; :: thesis: west_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 ) } = west_halfline p by TOPREAL1:36;
(min ((W-bound (L~ (Cage (C,n)))),(p `1))) - 1 < (W-bound (L~ (Cage (C,n)))) - 0 by XREAL_1:15, XXREAL_0:17;
then ( (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) & |[((min ((W-bound (L~ (Cage (C,n)))),(p `1))) - 1),(p `2)]| `1 < W-bound (L~ (Cage (C,n))) ) by EUCLID:52, JORDAN9:32;
then |[((min ((W-bound (L~ (Cage (C,n)))),(p `1))) - 1),(p `2)]| in LeftComp (Cage (C,n)) by JORDAN2C:110;
then A3: |[((min ((W-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;
min ((W-bound (L~ (Cage (C,n)))),(p `1)) <= p `1 by XXREAL_0:17;
then (min ((W-bound (L~ (Cage (C,n)))),(p `1))) - 1 <= (p `1) - 0 by XREAL_1:13;
then A6: |[((min ((W-bound (L~ (Cage (C,n)))),(p `1))) - 1),(p `2)]| `1 <= p `1 by EUCLID:52;
|[((min ((W-bound (L~ (Cage (C,n)))),(p `1))) - 1),(p `2)]| `2 = p `2 by EUCLID:52;
then |[((min ((W-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 west_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