let T be non empty TopSpace; :: thesis:
let A be Subset of T; :: thesis:
let x be Point of T; :: thesis:
reconsider F = NeighborhoodSystem x as proper Filter of (BoolePoset ([#] T)) ;

hereby :: thesis:

assume x in Cl A ; :: thesis:
then reconsider N = (a_net F) " A as subnet of a_net F by Th18, YELLOW_6:22;
reconsider N9 = N as net of T ;
take N9 = N9; :: thesis:
thus N9 is_eventually_in A by YELLOW_6:23; :: thesis:
x is_a_convergence_point_of F,T by Th3;
then A1: x in Lim (a_net F) by Th17;
Lim (a_net F) c= Lim N by YELLOW_6:32;
hence x is_a_cluster_point_of N9 by A1, WAYBEL_9:29; :: thesis:

end;

given N being net of T such that A2: N is_eventually_in A and
A3: x is_a_cluster_point_of N ; :: thesis:
consider i being Element of N such that
A4: for j being Element of N st i <= j holds
N . j in A by A2;

let G be Subset of T; :: thesis:
assume that
A5: G is open and
A6: x in G ; :: thesis:
Int G = G by A5, TOPS_1:23;
then G is a_neighborhood of x by A6, CONNSP_2:def 1;
then N is_often_in G by A3;
then consider j being Element of N such that
A7: i <= j and
A8: N . j in G ;
N . j in A by A4, A7;
hence A meets G by A8, XBOOLE_0:3; :: thesis:

end;

hence x in Cl A by PRE_TOPC:def 7; :: thesis: