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 (south_halfline x) /\ (L~ (Cage C,n)) holds
p `2 < x `2
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 (south_halfline x) /\ (L~ (Cage C,n)) holds
p `2 < x `2
let x, p be Point of (TOP-REAL 2); :: thesis: ( x in C & p in (south_halfline x) /\ (L~ (Cage C,n)) implies p `2 < x `2 )
set f = Cage C,n;
assume A1: x in C ; :: thesis: ( not p in (south_halfline x) /\ (L~ (Cage C,n)) or p `2 < x `2 )
assume A2: p in (south_halfline x) /\ (L~ (Cage C,n)) ; :: thesis: p `2 < x `2
then A3: p in south_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 14;
A6: p `2 <= x `2 by A3, TOPREAL1:def 14;
assume p `2 >= x `2 ; :: thesis: contradiction
then p `2 = x `2 by A6, XXREAL_0:1;
then p = x by A5, 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