let n be Element of 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 N-most C holds
ex p being Point of (TOP-REAL 2) st (north_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 N-most C holds
ex p being Point of (TOP-REAL 2) st (north_halfline x) /\ (L~ (Cage (C,n))) = {p}
let x be Point of (TOP-REAL 2); :: thesis: ( x in N-most C implies ex p being Point of (TOP-REAL 2) st (north_halfline x) /\ (L~ (Cage (C,n))) = {p} )
set f = Cage (C,n);
assume A1: x in N-most C ; :: thesis: ex p being Point of (TOP-REAL 2) st (north_halfline x) /\ (L~ (Cage (C,n))) = {p}
then x in C by XBOOLE_0:def 4;
then north_halfline x meets L~ (Cage (C,n)) by Th72;
then consider p being set such that
A2: p in north_halfline x and
A3: p in L~ (Cage (C,n)) by XBOOLE_0:3;
A4: p in (north_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: (north_halfline x) /\ (L~ (Cage (C,n))) = {p}

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

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

end;

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