for T being non empty TopSpace st T is T_2 holds
for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff ( S is convergent & x = lim S ) )