for T being non empty TopStruct
for x being Point of T
for S being sequence of T st S = NAT --> x holds
S is_convergent_to x