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
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:43;
(min (W-bound (L~ (Cage C,n))),(p `1 )) - 1 < (W-bound (L~ (Cage C,n))) - 0 by XREAL_1:17, 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:56, JORDAN9:34;
then |[((min (W-bound (L~ (Cage C,n))),(p `1 )) - 1),(p `2 )]| in LeftComp (Cage C,n) by JORDAN2C:118;
then A3: |[((min (W-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;
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:15;
then A6: |[((min (W-bound (L~ (Cage C,n))),(p `1 )) - 1),(p `2 )]| `1 <= p `1 by EUCLID:56;
|[((min (W-bound (L~ (Cage C,n))),(p `1 )) - 1),(p `2 )]| `2 = p `2 by EUCLID:56;
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: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