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
south_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
south_halfline p meets L~ (Cage (C,n))
let p be Point of (TOP-REAL 2); :: thesis: ( p in C implies south_halfline p meets L~ (Cage (C,n)) )
set f = Cage (C,n);
assume A1: p in C ; :: thesis: south_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 ) } = south_halfline p by TOPREAL1:34;
(min ((S-bound (L~ (Cage (C,n)))),(p `2))) - 1 < (S-bound (L~ (Cage (C,n)))) - 0 by XREAL_1:15, XXREAL_0:17;
then ( (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) & |[(p `1),((min ((S-bound (L~ (Cage (C,n)))),(p `2))) - 1)]| `2 < S-bound (L~ (Cage (C,n))) ) by EUCLID:52, JORDAN9:32;
then |[(p `1),((min ((S-bound (L~ (Cage (C,n)))),(p `2))) - 1)]| in LeftComp (Cage (C,n)) by JORDAN2C:112;
then A3: |[(p `1),((min ((S-bound (L~ (Cage (C,n)))),(p `2))) - 1)]| 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 ((S-bound (L~ (Cage (C,n)))),(p `2)) <= p `2 by XXREAL_0:17;
then (min ((S-bound (L~ (Cage (C,n)))),(p `2))) - 1 <= (p `2) - 0 by XREAL_1:13;
then A6: |[(p `1),((min ((S-bound (L~ (Cage (C,n)))),(p `2))) - 1)]| `2 <= p `2 by EUCLID:52;
|[(p `1),((min ((S-bound (L~ (Cage (C,n)))),(p `2))) - 1)]| `1 = p `1 by EUCLID:52;
then |[(p `1),((min ((S-bound (L~ (Cage (C,n)))),(p `2))) - 1)]| in X by A6;
then A7: X meets UBD (L~ (Cage (C,n))) by A3, XBOOLE_0:3;
assume not south_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