let T be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: x in Lim N

now

defpred S₁[ set , set ] means for i, j being Element of N st i = $2 & j >= i holds
N . j in $1;
let A be a_neighborhood of x; :: thesis: N is_eventually_in A
Int A is open by TOPS_1:51;
then A2: Int A in the topology of T by PRE_TOPC:def 5;
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 4;
A10: for a being set st a in Z holds
ex b being set st
( b in the carrier of N & S₁[a,b] )

proof

let a be set ; :: thesis: ( a in Z implies ex b being set st
( b in the carrier of N & S₁[a,b] ) )
assume A11: a in Z ; :: thesis: ex b being set st
( b in the carrier of N & S₁[a,b] )
then reconsider a = a as Subset of T ;
x in a by A5, A9, A11, SETFAM_1:58;
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 by WAYBEL_0:def 11;
take i ; :: thesis: ( i in the carrier of N & S₁[a,i] )
thus ( i in the carrier of N & S₁[a,i] ) by A12; :: thesis: verum

end;

consider f being Function such that
A13: ( dom f = Z & rng f c= the carrier of N ) and
A14: for a being set st a in Z holds
S₁[a,f . a] from WELLORD2:sch 1(A10);
reconsider z = rng f as finite Subset of ([#] N) by A8, A13, FINSET_1:26;
[#] 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 :: thesis: verum

proof

take k ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not k <= b₁ or N . b₁ in A )
let i be Element of N; :: thesis: ( not k <= i or N . i in A )
A16: Int A c= A by TOPS_1:44;
assume A17: i >= k ; :: thesis: N . i in A

now

let a be set ; :: thesis: ( a in Z implies N . i in a )
assume A18: a in Z ; :: thesis: N . i in a
then A19: f . a in z by A13, FUNCT_1:def 5;
then reconsider j = f . a as Element of N ;
j <= k by A15, A19, LATTICE3:def 9;
hence N . i in a by A14, A17, A18, ORDERS_2:26; :: thesis: verum

end;

then A20: N . i in y by A9, SETFAM_1:58;
y c= union Y by A6, ZFMISC_1:92;
then N . i in Int A by A20, A4;
hence N . i in A by A16; :: thesis: verum

end;

end;

hence x in Lim N by YELLOW_6:def 18; :: thesis: verum