:: deftheorem Def2 defines lim FRECHET2:def 2 :
for T being non empty TopSpace
for S being sequence of T st ex x being Point of T st Lim S = {x} holds
for b₃ being Point of T holds
( b₃ = lim S iff S is_convergent_to b₃ );