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 (east_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 (east_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 (east_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 (east_halfline x) /\ (L~ (Cage (C,n))) or p `1 > x `1 )
assume A2: p in (east_halfline x) /\ (L~ (Cage (C,n))) ; :: thesis: p `1 > x `1
then A3: p in east_halfline x by XBOOLE_0:def 4;
then A4: p `2 = x `2 by TOPREAL1:def 11;
assume A5: p `1 <= x `1 ; :: thesis: contradiction
p `1 >= x `1 by A3, TOPREAL1:def 11;
then p `1 = x `1 by A5, XXREAL_0:1;
then A6: p = x by A4, TOPREAL3:6;
p in L~ (Cage (C,n)) by A2, XBOOLE_0:def 4;
then x in C /\ (L~ (Cage (C,n))) by A1, A6, XBOOLE_0:def 4;
then C meets L~ (Cage (C,n)) by XBOOLE_0:4;
hence contradiction by JORDAN10:5; :: thesis: verum