:: deftheorem Def2 defines Lim_sup KURATO_2:def 2 :
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b₃ being Subset of T holds
( b₃ = Lim_sup S iff for x being object holds
( x in b₃ iff ex A being subsequence of S st x in Lim_inf A ) );