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

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

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

end;

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