:: deftheorem Def5 defines convergent KURATO_0:def 5 :
for T being set
for S being SetSequence of T holds
( S is convergent iff lim_sup S = lim_inf S );