theorem :: FRECHET2:32

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