let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for p, x 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); for p, x 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 p, x be Point of (TOP-REAL 2); ( 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
; ( 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)))
; p `2 < x `2
then A3:
p in south_halfline x
by XBOOLE_0:def 4;
then A4:
p `1 = x `1
by TOPREAL1:def 12;
assume A5:
p `2 >= x `2
; contradiction
p `2 <= x `2
by A3, TOPREAL1:def 12;
then
p `2 = x `2
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))
;
hence
contradiction
by JORDAN10:5; verum