let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p being Point of (TOP-REAL 2) st x in C & p in (west_halfline x) /\ (L~ (Cage C,n)) holds
p `1 < x `1
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for x, p being Point of (TOP-REAL 2) st x in C & p in (west_halfline x) /\ (L~ (Cage C,n)) holds
p `1 < x `1
let x, p be Point of (TOP-REAL 2); :: thesis: ( x in C & p in (west_halfline x) /\ (L~ (Cage C,n)) implies p `1 < x `1 )
set f = Cage C,n;
assume A1: x in C ; :: thesis: ( not p in (west_halfline x) /\ (L~ (Cage C,n)) or p `1 < x `1 )
assume A2: p in (west_halfline x) /\ (L~ (Cage C,n)) ; :: thesis: p `1 < x `1
then A3: p in west_halfline x by XBOOLE_0:def 4;
A4: p in L~ (Cage C,n) by A2, XBOOLE_0:def 4;
A5: p `1 <= x `1 by A3, TOPREAL1:def 15;
A6: p `2 = x `2 by A3, TOPREAL1:def 15;
assume p `1 >= x `1 ; :: thesis: contradiction
then p `1 = x `1 by A5, XXREAL_0:1;
then p = x by A6, TOPREAL3:11;
then x in C /\ (L~ (Cage C,n)) by A1, A4, XBOOLE_0:def 4;
then C meets L~ (Cage C,n) by XBOOLE_0:4;
hence contradiction by JORDAN10:5; :: thesis: verum