for x being object
for T being non empty TopSpace
for cF being Filter of the carrier of T st x in lim_filter cF holds
x is_a_cluster_point_of cF,T