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 F being proper Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T ) )

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

( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T ) )

let x be Point of T; :: thesis: ( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T ) )

A4: x is_a_cluster_point_of F,T ; :: thesis: x in Cl A

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

A5: a_filter (a_net F9) = F by Th14;

then A6: x is_a_cluster_point_of a_net F9 by A4, Th11;

a_net F9 is_eventually_in A by A3, A5, Th10;

hence x in Cl A by A6, Th21; :: thesis: verum

for x being Point of T holds

( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T ) )

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

( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T ) )

let x be Point of T; :: thesis: ( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T ) )

hereby :: thesis: ( ex F being proper Filter of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T ) implies x in Cl A )

given F being proper Filter of (BoolePoset ([#] T)) such that A3:
A in F
and ( A in F & x is_a_cluster_point_of F,T ) implies x in Cl A )

assume
x in Cl A
; :: thesis: ex F being Subset of (BoolePoset ([#] T)) st

( A in F & x is_a_cluster_point_of F,T )

then consider N being net of T such that

A1: N is_eventually_in A and

A2: x is_a_cluster_point_of N by Th21;

set F = a_filter N;

take F = a_filter N; :: thesis: ( A in F & x is_a_cluster_point_of F,T )

thus A in F by A1; :: thesis: x is_a_cluster_point_of F,T

thus x is_a_cluster_point_of F,T by A2, Th11; :: thesis: verum

end;( A in F & x is_a_cluster_point_of F,T )

then consider N being net of T such that

A1: N is_eventually_in A and

A2: x is_a_cluster_point_of N by Th21;

set F = a_filter N;

take F = a_filter N; :: thesis: ( A in F & x is_a_cluster_point_of F,T )

thus A in F by A1; :: thesis: x is_a_cluster_point_of F,T

thus x is_a_cluster_point_of F,T by A2, Th11; :: thesis: verum

A4: x is_a_cluster_point_of F,T ; :: thesis: x in Cl A

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

A5: a_filter (a_net F9) = F by Th14;

then A6: x is_a_cluster_point_of a_net F9 by A4, Th11;

a_net F9 is_eventually_in A by A3, A5, Th10;

hence x in Cl A by A6, Th21; :: thesis: verum