for T being non empty TopStruct
for S being sequence of T
for x being Point of T st ex S1 being subsequence of S st S1 is_convergent_to x holds
x is_a_cluster_point_of S