let T be non empty TopSpace; for K being prebasis of T
for N being net of T
for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
let K be prebasis of T; for N being net of T
for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
let N be net of T; for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
let x be Point of T; ( ( for A being Subset of T st x in A & A in K holds
N is_eventually_in A ) implies x in Lim N )
assume A1:
for A being Subset of T st x in A & A in K holds
N is_eventually_in A
; x in Lim N
now for A being a_neighborhood of x holds N is_eventually_in Adefpred S1[
object ,
object ]
means ex
D1 being
set st
(
D1 = $1 & ( for
i,
j being
Element of
N st
i = $2 &
j >= i holds
N . j in D1 ) );
let A be
a_neighborhood of
x;
N is_eventually_in AA2:
Int A in the
topology of
T
by PRE_TOPC:def 2;
FinMeetCl K is
Basis of
T
by YELLOW_9:23;
then
the
topology of
T = UniCl (FinMeetCl K)
by YELLOW_9:22;
then consider Y being
Subset-Family of
T such that A3:
Y c= FinMeetCl K
and A4:
Int A = union Y
by A2, CANTOR_1:def 1;
x in Int A
by CONNSP_2:def 1;
then consider y being
set such that A5:
x in y
and A6:
y in Y
by A4, TARSKI:def 4;
consider Z being
Subset-Family of
T such that A7:
Z c= K
and A8:
Z is
finite
and A9:
y = Intersect Z
by A3, A6, CANTOR_1:def 3;
A10:
for
a being
object st
a in Z holds
ex
b being
object st
(
b in the
carrier of
N &
S1[
a,
b] )
proof
let a be
object ;
( a in Z implies ex b being object st
( b in the carrier of N & S1[a,b] ) )
assume A11:
a in Z
;
ex b being object st
( b in the carrier of N & S1[a,b] )
then reconsider a =
a as
Subset of
T ;
x in a
by A5, A9, A11, SETFAM_1:43;
then
N is_eventually_in a
by A1, A7, A11;
then consider i being
Element of
N such that A12:
for
j being
Element of
N st
j >= i holds
N . j in a
;
reconsider i =
i as
object ;
take
i
;
( i in the carrier of N & S1[a,i] )
thus
i in the
carrier of
N
;
S1[a,i]
take
a
;
( a = a & ( for i, j being Element of N st i = i & j >= i holds
N . j in a ) )
thus
(
a = a & ( for
i,
j being
Element of
N st
i = i &
j >= i holds
N . j in a ) )
by A12;
verum
end; consider f being
Function such that A13:
(
dom f = Z &
rng f c= the
carrier of
N )
and A14:
for
a being
object st
a in Z holds
S1[
a,
f . a]
from FUNCT_1:sch 6(A10);
reconsider z =
rng f as
finite Subset of
([#] N) by A8, A13, FINSET_1:8;
[#] N is
directed
by WAYBEL_0:def 6;
then consider k being
Element of
N such that
k in [#] N
and A15:
k is_>=_than z
by WAYBEL_0:1;
thus
N is_eventually_in A
verum end;
hence
x in Lim N
by YELLOW_6:def 15; verum