let n be Nat; 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); 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); ( 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
; 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 Th54;
then consider p being object 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
; (west_halfline x) /\ (L~ (Cage (C,n))) = {p}
hereby TARSKI:def 3,
XBOOLE_0:def 10 {p} c= (west_halfline x) /\ (L~ (Cage (C,n)))
let a be
object ;
( a in (west_halfline x) /\ (L~ (Cage (C,n))) implies a in {p} )assume A5:
a in (west_halfline x) /\ (L~ (Cage (C,n)))
;
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 13
.=
p `2
by A2, TOPREAL1:def 13
;
p `1 =
W-bound (L~ (Cage (C,n)))
by A1, A4, Th85
.=
y `1
by A1, A5, Th85
;
then
y = p
by A6, TOPREAL3:6;
hence
a in {p}
by TARSKI:def 1;
verum
end;
thus
{p} c= (west_halfline x) /\ (L~ (Cage (C,n)))
by A4, ZFMISC_1:31; verum