let T be non empty TopSpace; :: thesis: for A being Subset of T

for x being Point of T holds

( x in Cl A iff ex N being net of T st

( N is_eventually_in A & x is_a_cluster_point_of N ) )

let A be Subset of T; :: thesis: for x being Point of T holds

( x in Cl A iff ex N being net of T st

( N is_eventually_in A & x is_a_cluster_point_of N ) )

let x be Point of T; :: thesis: ( x in Cl A iff ex N being net of T st

( N is_eventually_in A & x is_a_cluster_point_of N ) )

reconsider F = NeighborhoodSystem x as proper Filter of (BoolePoset ([#] T)) ;

A3: x is_a_cluster_point_of N ; :: thesis: x in Cl A

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;

for x being Point of T holds

( x in Cl A iff ex N being net of T st

( N is_eventually_in A & x is_a_cluster_point_of N ) )

let A be Subset of T; :: thesis: for x being Point of T holds

( x in Cl A iff ex N being net of T st

( N is_eventually_in A & x is_a_cluster_point_of N ) )

let x be Point of T; :: thesis: ( x in Cl A iff ex N being net of T 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 T st

( N is_eventually_in A & x is_a_cluster_point_of N ) implies x in Cl A )

given N being net of T such that A2:
N is_eventually_in A
and ( N is_eventually_in A & x is_a_cluster_point_of N ) implies x in Cl A )

assume
x in Cl A
; :: thesis: ex N9 being net of T st

( N9 is_eventually_in A & x is_a_cluster_point_of N9 )

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: ( N9 is_eventually_in A & x is_a_cluster_point_of N9 )

thus N9 is_eventually_in A by YELLOW_6:23; :: thesis: x is_a_cluster_point_of N9

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: verum

end;( N9 is_eventually_in A & x is_a_cluster_point_of N9 )

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: ( N9 is_eventually_in A & x is_a_cluster_point_of N9 )

thus N9 is_eventually_in A by YELLOW_6:23; :: thesis: x is_a_cluster_point_of N9

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: verum

A3: x is_a_cluster_point_of N ; :: thesis: x in Cl A

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;

now :: thesis: for G being Subset of T st G is open & x in G holds

A meets G

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

let G be Subset of T; :: 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: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: verum

end;assume that

A5: G is open and

A6: x in G ; :: thesis: A meets G

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: verum