:: deftheorem defines is_convergent_to FRECHET:def 3 :
for T being TopStruct
for S being sequence of T
for x being Point of T holds
( S is_convergent_to x iff for U1 being Subset of T st U1 is open & x in U1 holds
ex n being Nat st
for m being Nat st n <= m holds
S . m in U1 );