:: deftheorem Def2 defines lim_sup KURATO_0:def 2 :
for X being set
for F being SetSequence of X
for b₃ being Subset of X holds
( b₃ = lim_sup F iff ex f being SetSequence of X st
( b₃ = meet f & ( for n being Nat holds f . n = Union (F ^\ n) ) ) );