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

now :: thesis:

let Z be finite Subset-Family of T; :: thesis:
assume that
A4: Z c= BB and
A5: x in Intersect Z ; :: thesis:
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:

let a be object ; :: thesis:
assume A7: a in Z ; :: thesis:
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:
thus ( b in the carrier of N & S₁[a,b] ) by A8; :: thesis:

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 by A9, RELAT_1:42;

suppose Z = {} ; :: thesis:

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:

end;

suppose rng f <> {} ; :: thesis:

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:

let y be set ; :: thesis:
assume A12: y in Z ; :: thesis:
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:

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:

end;

end;

end;

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