for L being non empty Hausdorff compact TopSpace
for N being net of L st ( for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds
c = d ) holds
for s being Point of L st s is_a_cluster_point_of N holds
s in Lim N