let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x being Point of (TOP-REAL 2) st x in S-most C holds
ex p being Point of (TOP-REAL 2) st (south_halfline x) /\ (L~ (Cage (C,n))) = {p}
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for x being Point of (TOP-REAL 2) st x in S-most C holds
ex p being Point of (TOP-REAL 2) st (south_halfline x) /\ (L~ (Cage (C,n))) = {p}
let x be Point of (TOP-REAL 2); :: thesis: ( x in S-most C implies ex p being Point of (TOP-REAL 2) st (south_halfline x) /\ (L~ (Cage (C,n))) = {p} )
set f = Cage (C,n);
assume A1: x in S-most C ; :: thesis: ex p being Point of (TOP-REAL 2) st (south_halfline x) /\ (L~ (Cage (C,n))) = {p}
then x in C by XBOOLE_0:def 4;
then south_halfline x meets L~ (Cage (C,n)) by Th53;
then consider p being object such that
A2: p in south_halfline x and
A3: p in L~ (Cage (C,n)) by XBOOLE_0:3;
A4: p in (south_halfline x) /\ (L~ (Cage (C,n))) by A2, A3, XBOOLE_0:def 4;
reconsider p = p as Point of (TOP-REAL 2) by A2;
take p ; :: thesis: (south_halfline x) /\ (L~ (Cage (C,n))) = {p}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {p} c= (south_halfline x) /\ (L~ (Cage (C,n)))

let a be object ; :: thesis: ( a in (south_halfline x) /\ (L~ (Cage (C,n))) implies a in {p} )
assume A5: a in (south_halfline x) /\ (L~ (Cage (C,n))) ; :: thesis: a in {p}
then reconsider y = a as Point of (TOP-REAL 2) ;
y in south_halfline x by A5, XBOOLE_0:def 4;
then A6: y `1 = x `1 by TOPREAL1:def 12
.= p `1 by A2, TOPREAL1:def 12 ;
p `2 = S-bound (L~ (Cage (C,n))) by A1, A4, Th84
.= y `2 by A1, A5, Th84 ;
then y = p by A6, TOPREAL3:6;
hence a in {p} by TARSKI:def 1; :: thesis: verum

end;

thus {p} c= (south_halfline x) /\ (L~ (Cage (C,n))) by A4, ZFMISC_1:31; :: thesis: verum