for T being non empty TopStruct
for S being sequence of T
for x being Point of T
for Y being Subset of T st Y = { y where y is Point of T : x in Cl {y} } & rng S c= Y holds
S is_convergent_to x