:: deftheorem defines convergent FRECHET:def 4 :
for T being TopStruct
for S being sequence of T holds
( S is convergent iff ex x being Point of T st S is_convergent_to x );