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

( A in F & x is_a_convergence_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 ultra Filter of (BoolePoset ([#] T)) st

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

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

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

A7: x is_a_convergence_point_of F,T ; :: thesis: x in Cl A

x is_a_cluster_point_of F,T by A7, WAYBEL_7:27;

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

for x being Point of T holds

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

( A in F & x is_a_convergence_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 ultra Filter of (BoolePoset ([#] T)) st

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

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

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

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

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

given F being ultra Filter of (BoolePoset ([#] T)) such that A6:
A in F
and ( A in F & x is_a_convergence_point_of F,T ) implies x in Cl A )

assume
x in Cl A
; :: thesis: ex G being ultra Filter of (BoolePoset ([#] T)) st

( A in G & x is_a_convergence_point_of G,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;

consider S being subnet of N such that

A3: x in Lim S by A2, WAYBEL_9:32;

set F = a_filter S;

consider G being Filter of (BoolePoset ([#] T)) such that

A4: a_filter S c= G and

A5: G is ultra by WAYBEL_7:26;

reconsider G = G as ultra Filter of (BoolePoset ([#] T)) by A5;

take G = G; :: thesis: ( A in G & x is_a_convergence_point_of G,T )

S is_eventually_in A by A1, Th19;

then A in a_filter S ;

hence A in G by A4; :: thesis: x is_a_convergence_point_of G,T

x is_a_convergence_point_of a_filter S,T by A3, Th12;

hence x is_a_convergence_point_of G,T by A4; :: thesis: verum

end;( A in G & x is_a_convergence_point_of G,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;

consider S being subnet of N such that

A3: x in Lim S by A2, WAYBEL_9:32;

set F = a_filter S;

consider G being Filter of (BoolePoset ([#] T)) such that

A4: a_filter S c= G and

A5: G is ultra by WAYBEL_7:26;

reconsider G = G as ultra Filter of (BoolePoset ([#] T)) by A5;

take G = G; :: thesis: ( A in G & x is_a_convergence_point_of G,T )

S is_eventually_in A by A1, Th19;

then A in a_filter S ;

hence A in G by A4; :: thesis: x is_a_convergence_point_of G,T

x is_a_convergence_point_of a_filter S,T by A3, Th12;

hence x is_a_convergence_point_of G,T by A4; :: thesis: verum

A7: x is_a_convergence_point_of F,T ; :: thesis: x in Cl A

x is_a_cluster_point_of F,T by A7, WAYBEL_7:27;

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