let T be non empty TopSpace; :: thesis:
let A be Subset of T; :: thesis:
let x be Point of T; :: thesis:

hereby :: thesis:

assume x in Cl A ; :: thesis:
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:
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 a_filter S,T by A3, Th12;
hence x is_a_convergence_point_of G,T by A4; :: thesis:

end;

given F being ultra Filter of (BoolePoset ([#] T)) such that A6: A in F and
A7: x is_a_convergence_point_of F,T ; :: thesis:
x is_a_cluster_point_of F,T by A7, WAYBEL_7:27;
hence x in Cl A by A6, Th25; :: thesis: