let n be Nat; 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); 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); ( p in C implies west_halfline p meets L~ (Cage (C,n)) )
set f = Cage (C,n);
assume A1:
p in C
; 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))
; 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; verum