for L being non empty TopSpace
for N being net of L
for c being Point of L st c in Lim N holds
c is_a_cluster_point_of N