let T be non empty TopSpace; :: thesis: for K being prebasis of T
for x being Point of T
for N being net of T st ( for A being Subset of T st A in K & x in A holds
N is_eventually_in A ) holds
for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
let BB be prebasis of T; :: thesis: for x being Point of T
for N being net of T st ( for A being Subset of T st A in BB & x in A holds
N is_eventually_in A ) holds
for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
let x be Point of T; :: thesis: for N being net of T st ( for A being Subset of T st A in BB & x in A holds
N is_eventually_in A ) holds
for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
let N be net of T; :: thesis: ( ( for A being Subset of T st A in BB & x in A holds
N is_eventually_in A ) implies for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S )
assume A1: for A being Subset of T st A in BB & x in A holds
N is_eventually_in A ; :: thesis: for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
let S be Subset of T; :: thesis: ( rng (netmap (N,T)) c= S implies x in Cl S )
assume A2: rng (netmap (N,T)) c= S ; :: thesis: x in Cl S
A3: [#] N is directed by WAYBEL_0:def 6;

now :: thesis: for Z being finite Subset-Family of T st Z c= BB & x in Intersect Z holds
Intersect Z meets S

let Z be finite Subset-Family of T; :: thesis: ( Z c= BB & x in Intersect Z implies Intersect b₁ meets S )
assume that
A4: Z c= BB and
A5: x in Intersect Z ; :: thesis: Intersect b₁ meets S
defpred S₁[ object , object ] means for i, j being Element of N st $2 = i & i <= j holds
ex pp being set st
( pp = $1 & N . j in pp );

A6: now :: thesis: for a being object st a in Z holds
ex b being object st
( b in the carrier of N & S₁[a,b] )

let a be object ; :: thesis: ( a in Z implies ex b being object st
( b in the carrier of N & S₁[a,b] ) )
assume A7: a in Z ; :: thesis: ex b being object st
( b in the carrier of N & S₁[a,b] )
then reconsider A = a as Subset of T ;
x in A by A5, A7, SETFAM_1:43;
then N is_eventually_in A by A1, A4, A7;
then consider i being Element of N such that
A8: for j being Element of N st i <= j holds
N . j in A ;
reconsider b = i as object ;
take b = b; :: thesis: ( b in the carrier of N & S₁[a,b] )
thus ( b in the carrier of N & S₁[a,b] ) by A8; :: thesis: verum

end;

consider f being Function such that
A9: ( dom f = Z & rng f c= the carrier of N & ( for a being object st a in Z holds
S₁[a,f . a] ) ) from FUNCT_1:sch 6(A6);
set k = the Element of N;

per cases ( Z = {} or rng f <> {} ) by A9, RELAT_1:42;

suppose Z = {} ; :: thesis: Intersect b₁ meets S

then A10: Intersect Z = the carrier of T by SETFAM_1:def 9;
N . the Element of N in rng (netmap (N,T)) by FUNCT_2:4;
hence Intersect Z meets S by A2, A10, XBOOLE_0:3; :: thesis: verum

end;

suppose rng f <> {} ; :: thesis: Intersect b₁ meets S

then reconsider Y = rng f as non empty finite Subset of N by A9, FINSET_1:8;
consider i being Element of N such that
i in the carrier of N and
A11: i is_>=_than Y by A3, WAYBEL_0:1;

now :: thesis: for y being set st y in Z holds
N . i in y

let y be set ; :: thesis: ( y in Z implies N . i in y )
assume A12: y in Z ; :: thesis: N . i in y
then A13: f . y in Y by A9, FUNCT_1:def 3;
then reconsider j = f . y as Element of N ;
A14: j <= i by A11, A13, LATTICE3:def 9;
S₁[y,j] by A9, A12;
then ex pp being set st
( pp = y & N . i in pp ) by A14;
hence N . i in y ; :: thesis: verum

end;

then A15: N . i in Intersect Z by SETFAM_1:43;
N . i in rng (netmap (N,T)) by FUNCT_2:4;
hence Intersect Z meets S by A2, A15, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

hence x in Cl S by Th38; :: thesis: verum