let T be non empty TopSpace; :: thesis: for A being Subset of
for x being Point of holds
( x in Cl A iff ex N being net of st
( N is_eventually_in A & x is_a_cluster_point_of N ) )
let A be Subset of ; :: thesis: for x being Point of holds
( x in Cl A iff ex N being net of st
( N is_eventually_in A & x is_a_cluster_point_of N ) )
let x be Point of ; :: thesis: ( x in Cl A iff ex N being net of st
( N is_eventually_in A & x is_a_cluster_point_of N ) )
reconsider F = NeighborhoodSystem x as proper Filter of BoolePoset ([#] T) ;

hereby :: thesis: ( ex N being net of st
( N is_eventually_in A & x is_a_cluster_point_of N ) implies x in Cl A )

assume x in Cl A ; :: thesis: ex N' being net of st
( N' is_eventually_in A & x is_a_cluster_point_of N' )
then reconsider N = (a_net F) " A as subnet of a_net F by Th20, YELLOW_6:31;
reconsider N' = N as net of ;
take N' = N'; :: thesis: ( N' is_eventually_in A & x is_a_cluster_point_of N' )
thus N' is_eventually_in A by YELLOW_6:32; :: thesis: x is_a_cluster_point_of N'
x is_a_convergence_point_of F,T by Th4;
then A1: x in Lim (a_net F) by Th18;
Lim (a_net F) c= Lim N by YELLOW_6:41;
hence x is_a_cluster_point_of N' by A1, WAYBEL_9:29; :: thesis: verum

end;

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

now

let G be Subset of ; :: thesis: ( G is open & x in G implies A meets G )
assume that
A5: G is open and
A6: x in G ; :: thesis: A meets G
Int G = G by A5, TOPS_1:55;
then G is a_neighborhood of x by A6, CONNSP_2:def 1;
then N is_often_in G by A3, WAYBEL_9:def 9;
then consider j being Element of such that
A7: i <= j and
A8: N . j in G by WAYBEL_0:def 12;
N . j in A by A4, A7;
hence A meets G by A8, XBOOLE_0:3; :: thesis: verum

end;

hence x in Cl A by PRE_TOPC:def 13; :: thesis: verum