:: deftheorem Def5 defines Lim FRECHET:def 5 :
for T being non empty TopStruct
for S being sequence of T
for b₃ being Subset of T holds
( b₃ = Lim S iff for x being Point of T holds
( x in b₃ iff S is_convergent_to x ) );